Termination proof of /tmp/tmprHr93D/BubbleSortR.jar

Termination of the given JBC could be proven:

0 JBC

↳1 JBC2FIG (⇐)

↳2 FIGraph

↳3 FIGtoITRSProof (⇐)

↳4 AND

    ↳5 ITRS

        ↳6 GroundTermsRemoverProof (⇔)

        ↳7 ITRS

        ↳8 DuplicateArgsRemoverProof (⇔)

        ↳9 ITRS

        ↳10 ITRStoIDPProof (⇔)

        ↳11 IDP

        ↳12 UsableRulesProof (⇔)

        ↳13 IDP

        ↳14 ItpfGraphProof (⇔)

        ↳15 IDP

        ↳16 IDPNonInfProof (⇐)

        ↳17 AND

            ↳18 IDP

                ↳19 IDependencyGraphProof (⇔)

                ↳20 IDP

                ↳21 IDPNonInfProof (⇐)

                ↳22 AND

                    ↳23 IDP

                        ↳24 IDependencyGraphProof (⇔)

                        ↳25 TRUE

                    ↳26 IDP

                        ↳27 IDependencyGraphProof (⇔)

                        ↳28 TRUE

            ↳29 IDP

                ↳30 IDependencyGraphProof (⇔)

                ↳31 IDP

                ↳32 IDPNonInfProof (⇐)

                ↳33 AND

                    ↳34 IDP

                        ↳35 IDependencyGraphProof (⇔)

                        ↳36 TRUE

                    ↳37 IDP

                        ↳38 IDependencyGraphProof (⇔)

                        ↳39 TRUE

    ↳40 ITRS

        ↳41 DuplicateArgsRemoverProof (⇔)

        ↳42 ITRS

        ↳43 ITRStoIDPProof (⇔)

        ↳44 IDP

        ↳45 UsableRulesProof (⇔)

        ↳46 IDP

        ↳47 ItpfGraphProof (⇔)

        ↳48 IDP

        ↳49 IDPNonInfProof (⇐)

        ↳50 AND

            ↳51 IDP

                ↳52 IDependencyGraphProof (⇔)

                ↳53 IDP

                ↳54 IDPNonInfProof (⇐)

                ↳55 AND

                    ↳56 IDP

                        ↳57 IDependencyGraphProof (⇔)

                        ↳58 TRUE

                    ↳59 IDP

                        ↳60 IDependencyGraphProof (⇔)

                        ↳61 TRUE

            ↳62 IDP

                ↳63 IDependencyGraphProof (⇔)

                ↳64 TRUE

(0) Obligation:

JBC Problem based on JBC Program:

No human-readable program information known.

Manifest-Version: 1.0 Created-By: 1.6.0_20 (Apple Inc.) Main-Class: BubbleSortR

(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
Graph of 500 nodes with 2 SCCs.

(3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph to ITRS rules

(4) Complex Obligation (AND)

(5) Obligation:

ITRS problem:

The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The TRS R consists of the following rules:
Load2339(java.lang.Object(ARRAY(i303, a2291data)), i303, i304) → Cond_Load2339(i304 > 0 && i304 < i303, java.lang.Object(ARRAY(i303, a2291data)), i303, i304)
Cond_Load2339(TRUE, java.lang.Object(ARRAY(i303, a2291data)), i303, i304) → Load3443(java.lang.Object(ARRAY(i303, a2291data)), i303, i304, 0, i303 - i304, java.lang.Object(ARRAY(i303, a2291data)), 0, i303 - i304, java.lang.Object(ARRAY(i303, a2291data)))
Load3657(java.lang.Object(ARRAY(i663, a3434data)), i663, i304, 0, i662, java.lang.Object(ARRAY(i663, a3434data)), i661, i662, java.lang.Object(ARRAY(i663, a3434data))) → Load3443(java.lang.Object(ARRAY(i663, a3434data)), i663, i304, 0, i662, java.lang.Object(ARRAY(i663, a3434data)), i661 + 1, i662, java.lang.Object(ARRAY(i663, a3434data)))
Load3443(java.lang.Object(ARRAY(i663, a3434data)), i663, i304, 0, i662, java.lang.Object(ARRAY(i663, a3434data)), i661, i662, java.lang.Object(ARRAY(i663, a3434data))) → Load3443ARR1(java.lang.Object(ARRAY(i663, a3434data)), i663, i304, 0, i662, java.lang.Object(ARRAY(i663, a3434data)), i661, i662, java.lang.Object(ARRAY(i663, a3434data)), i706, i677)
Load3443ARR1(java.lang.Object(ARRAY(i663, a3434data)), i663, i304, 0, i662, java.lang.Object(ARRAY(i663, a3434data)), i661, i662, java.lang.Object(ARRAY(i663, a3434data)), i706, i677) → Cond_Load3443ARR1(i677 <= i706 && i661 + 1 > 0 && i661 + 1 < i663 && i661 >= 0 && i661 < i663 && i661 < i662 && i661 + 1 > 0, java.lang.Object(ARRAY(i663, a3434data)), i663, i304, 0, i662, java.lang.Object(ARRAY(i663, a3434data)), i661, i662, java.lang.Object(ARRAY(i663, a3434data)), i706, i677)
Cond_Load3443ARR1(TRUE, java.lang.Object(ARRAY(i663, a3434data)), i663, i304, 0, i662, java.lang.Object(ARRAY(i663, a3434data)), i661, i662, java.lang.Object(ARRAY(i663, a3434data)), i706, i677) → Load3443(java.lang.Object(ARRAY(i663, a3434data)), i663, i304, 0, i662, java.lang.Object(ARRAY(i663, a3434data)), i661 + 1, i662, java.lang.Object(ARRAY(i663, a3434data)))
Load3443(java.lang.Object(ARRAY(i663, a3434data)), i663, i304, 0, i662, java.lang.Object(ARRAY(i663, a3434data)), i661, i662, java.lang.Object(ARRAY(i663, a3434data))) → Load3443ARR2(java.lang.Object(ARRAY(i663, a3434data)), i663, i304, 0, i662, java.lang.Object(ARRAY(i663, a3434data)), i661, i662, java.lang.Object(ARRAY(i663, a3434data)), i977, i790, i706, i677)
Load3443ARR2(java.lang.Object(ARRAY(i663, a3434data)), i663, i304, 0, i662, java.lang.Object(ARRAY(i663, a3434data)), i661, i662, java.lang.Object(ARRAY(i663, a3434data)), i977, i790, i706, i677) → Cond_Load3443ARR2(i661 + 1 > 0 && i661 + 1 < i663 && i661 >= 0 && i661 < i663 && i661 + 1 > 0 && i661 + 1 < i663 && i677 > i706 && i661 + 1 > 0 && i661 + 1 < i663 && i661 < i662, java.lang.Object(ARRAY(i663, a3434data)), i663, i304, 0, i662, java.lang.Object(ARRAY(i663, a3434data)), i661, i662, java.lang.Object(ARRAY(i663, a3434data)), i977, i790, i706, i677)
Cond_Load3443ARR2(TRUE, java.lang.Object(ARRAY(i663, a3434data)), i663, i304, 0, i662, java.lang.Object(ARRAY(i663, a3434data)), i661, i662, java.lang.Object(ARRAY(i663, a3434data)), i977, i790, i706, i677) → Load3657(java.lang.Object(ARRAY(i663, a3434dataNew)), i663, i304, 0, i662, java.lang.Object(ARRAY(i663, a3434dataNew)), i661, i662, java.lang.Object(ARRAY(i663, a3434dataNew)))
Load3443(java.lang.Object(ARRAY(i663, a3434data)), i663, i304, 0, i662, java.lang.Object(ARRAY(i663, a3434data)), i661, i662, java.lang.Object(ARRAY(i663, a3434data))) → Cond_Load3443(i661 >= i662 && i304 > 0 && i304 + 1 > 0, java.lang.Object(ARRAY(i663, a3434data)), i663, i304, 0, i662, java.lang.Object(ARRAY(i663, a3434data)), i661, i662, java.lang.Object(ARRAY(i663, a3434data)))
Cond_Load3443(TRUE, java.lang.Object(ARRAY(i663, a3434data)), i663, i304, 0, i662, java.lang.Object(ARRAY(i663, a3434data)), i661, i662, java.lang.Object(ARRAY(i663, a3434data))) → Load2339(java.lang.Object(ARRAY(i663, a3434data)), i663, i304 + 1)
The set Q consists of the following terms:
Load2339(java.lang.Object(ARRAY(x0, x1)), x0, x2)
Cond_Load2339(TRUE, java.lang.Object(ARRAY(x0, x1)), x0, x2)
Load3657(java.lang.Object(ARRAY(x0, x1)), x0, x2, 0, x3, java.lang.Object(ARRAY(x0, x1)), x4, x3, java.lang.Object(ARRAY(x0, x1)))
Load3443(java.lang.Object(ARRAY(x0, x1)), x0, x2, 0, x3, java.lang.Object(ARRAY(x0, x1)), x4, x3, java.lang.Object(ARRAY(x0, x1)))
Load3443ARR1(java.lang.Object(ARRAY(x0, x1)), x0, x2, 0, x3, java.lang.Object(ARRAY(x0, x1)), x4, x3, java.lang.Object(ARRAY(x0, x1)), x5, x6)
Cond_Load3443ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x0, x2, 0, x3, java.lang.Object(ARRAY(x0, x1)), x4, x3, java.lang.Object(ARRAY(x0, x1)), x5, x6)
Load3443ARR2(java.lang.Object(ARRAY(x0, x1)), x0, x2, 0, x3, java.lang.Object(ARRAY(x0, x1)), x4, x3, java.lang.Object(ARRAY(x0, x1)), x5, x6, x7, x8)
Cond_Load3443ARR2(TRUE, java.lang.Object(ARRAY(x0, x1)), x0, x2, 0, x3, java.lang.Object(ARRAY(x0, x1)), x4, x3, java.lang.Object(ARRAY(x0, x1)), x5, x6, x7, x8)
Cond_Load3443(TRUE, java.lang.Object(ARRAY(x0, x1)), x0, x2, 0, x3, java.lang.Object(ARRAY(x0, x1)), x4, x3, java.lang.Object(ARRAY(x0, x1)))

(6) GroundTermsRemoverProof (EQUIVALENT transformation)

Some arguments are removed because they always contain the same ground term.
We removed the following ground terms:

We removed arguments according to the following replacements:

Cond_Load3443(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → Cond_Load3443(x1, x2, x3, x4, x6, x7, x8, x9, x10)
Load3657(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Load3657(x1, x2, x3, x5, x6, x7, x8, x9)
Cond_Load3443ARR2(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14) → Cond_Load3443ARR2(x1, x2, x3, x4, x6, x7, x8, x9, x10, x11, x12, x13, x14)
Load3443ARR2(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) → Load3443ARR2(x1, x2, x3, x5, x6, x7, x8, x9, x10, x11, x12, x13)
Cond_Load3443ARR1(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) → Cond_Load3443ARR1(x1, x2, x3, x4, x6, x7, x8, x9, x10, x11, x12)
Load3443ARR1(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) → Load3443ARR1(x1, x2, x3, x5, x6, x7, x8, x9, x10, x11)
Load3443(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Load3443(x1, x2, x3, x5, x6, x7, x8, x9)

(7) Obligation:

ITRS problem:

The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The TRS R consists of the following rules:
Load2339(java.lang.Object(ARRAY(i303, a2291data)), i303, i304) → Cond_Load2339(i304 > 0 && i304 < i303, java.lang.Object(ARRAY(i303, a2291data)), i303, i304)
Cond_Load2339(TRUE, java.lang.Object(ARRAY(i303, a2291data)), i303, i304) → Load3443(java.lang.Object(ARRAY(i303, a2291data)), i303, i304, i303 - i304, java.lang.Object(ARRAY(i303, a2291data)), 0, i303 - i304, java.lang.Object(ARRAY(i303, a2291data)))
Load3657(java.lang.Object(ARRAY(i663, a3434data)), i663, i304, i662, java.lang.Object(ARRAY(i663, a3434data)), i661, i662, java.lang.Object(ARRAY(i663, a3434data))) → Load3443(java.lang.Object(ARRAY(i663, a3434data)), i663, i304, i662, java.lang.Object(ARRAY(i663, a3434data)), i661 + 1, i662, java.lang.Object(ARRAY(i663, a3434data)))
Load3443(java.lang.Object(ARRAY(i663, a3434data)), i663, i304, i662, java.lang.Object(ARRAY(i663, a3434data)), i661, i662, java.lang.Object(ARRAY(i663, a3434data))) → Load3443ARR1(java.lang.Object(ARRAY(i663, a3434data)), i663, i304, i662, java.lang.Object(ARRAY(i663, a3434data)), i661, i662, java.lang.Object(ARRAY(i663, a3434data)), i706, i677)
Load3443ARR1(java.lang.Object(ARRAY(i663, a3434data)), i663, i304, i662, java.lang.Object(ARRAY(i663, a3434data)), i661, i662, java.lang.Object(ARRAY(i663, a3434data)), i706, i677) → Cond_Load3443ARR1(i677 <= i706 && i661 + 1 > 0 && i661 + 1 < i663 && i661 >= 0 && i661 < i663 && i661 < i662 && i661 + 1 > 0, java.lang.Object(ARRAY(i663, a3434data)), i663, i304, i662, java.lang.Object(ARRAY(i663, a3434data)), i661, i662, java.lang.Object(ARRAY(i663, a3434data)), i706, i677)
Cond_Load3443ARR1(TRUE, java.lang.Object(ARRAY(i663, a3434data)), i663, i304, i662, java.lang.Object(ARRAY(i663, a3434data)), i661, i662, java.lang.Object(ARRAY(i663, a3434data)), i706, i677) → Load3443(java.lang.Object(ARRAY(i663, a3434data)), i663, i304, i662, java.lang.Object(ARRAY(i663, a3434data)), i661 + 1, i662, java.lang.Object(ARRAY(i663, a3434data)))
Load3443(java.lang.Object(ARRAY(i663, a3434data)), i663, i304, i662, java.lang.Object(ARRAY(i663, a3434data)), i661, i662, java.lang.Object(ARRAY(i663, a3434data))) → Load3443ARR2(java.lang.Object(ARRAY(i663, a3434data)), i663, i304, i662, java.lang.Object(ARRAY(i663, a3434data)), i661, i662, java.lang.Object(ARRAY(i663, a3434data)), i977, i790, i706, i677)
Load3443ARR2(java.lang.Object(ARRAY(i663, a3434data)), i663, i304, i662, java.lang.Object(ARRAY(i663, a3434data)), i661, i662, java.lang.Object(ARRAY(i663, a3434data)), i977, i790, i706, i677) → Cond_Load3443ARR2(i661 + 1 > 0 && i661 + 1 < i663 && i661 >= 0 && i661 < i663 && i661 + 1 > 0 && i661 + 1 < i663 && i677 > i706 && i661 + 1 > 0 && i661 + 1 < i663 && i661 < i662, java.lang.Object(ARRAY(i663, a3434data)), i663, i304, i662, java.lang.Object(ARRAY(i663, a3434data)), i661, i662, java.lang.Object(ARRAY(i663, a3434data)), i977, i790, i706, i677)
Cond_Load3443ARR2(TRUE, java.lang.Object(ARRAY(i663, a3434data)), i663, i304, i662, java.lang.Object(ARRAY(i663, a3434data)), i661, i662, java.lang.Object(ARRAY(i663, a3434data)), i977, i790, i706, i677) → Load3657(java.lang.Object(ARRAY(i663, a3434dataNew)), i663, i304, i662, java.lang.Object(ARRAY(i663, a3434dataNew)), i661, i662, java.lang.Object(ARRAY(i663, a3434dataNew)))
Load3443(java.lang.Object(ARRAY(i663, a3434data)), i663, i304, i662, java.lang.Object(ARRAY(i663, a3434data)), i661, i662, java.lang.Object(ARRAY(i663, a3434data))) → Cond_Load3443(i661 >= i662 && i304 > 0 && i304 + 1 > 0, java.lang.Object(ARRAY(i663, a3434data)), i663, i304, i662, java.lang.Object(ARRAY(i663, a3434data)), i661, i662, java.lang.Object(ARRAY(i663, a3434data)))
Cond_Load3443(TRUE, java.lang.Object(ARRAY(i663, a3434data)), i663, i304, i662, java.lang.Object(ARRAY(i663, a3434data)), i661, i662, java.lang.Object(ARRAY(i663, a3434data))) → Load2339(java.lang.Object(ARRAY(i663, a3434data)), i663, i304 + 1)
The set Q consists of the following terms:
Load2339(java.lang.Object(ARRAY(x0, x1)), x0, x2)
Cond_Load2339(TRUE, java.lang.Object(ARRAY(x0, x1)), x0, x2)
Load3657(java.lang.Object(ARRAY(x0, x1)), x0, x2, x3, java.lang.Object(ARRAY(x0, x1)), x4, x3, java.lang.Object(ARRAY(x0, x1)))
Load3443(java.lang.Object(ARRAY(x0, x1)), x0, x2, x3, java.lang.Object(ARRAY(x0, x1)), x4, x3, java.lang.Object(ARRAY(x0, x1)))
Load3443ARR1(java.lang.Object(ARRAY(x0, x1)), x0, x2, x3, java.lang.Object(ARRAY(x0, x1)), x4, x3, java.lang.Object(ARRAY(x0, x1)), x5, x6)
Cond_Load3443ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x0, x2, x3, java.lang.Object(ARRAY(x0, x1)), x4, x3, java.lang.Object(ARRAY(x0, x1)), x5, x6)
Load3443ARR2(java.lang.Object(ARRAY(x0, x1)), x0, x2, x3, java.lang.Object(ARRAY(x0, x1)), x4, x3, java.lang.Object(ARRAY(x0, x1)), x5, x6, x7, x8)
Cond_Load3443ARR2(TRUE, java.lang.Object(ARRAY(x0, x1)), x0, x2, x3, java.lang.Object(ARRAY(x0, x1)), x4, x3, java.lang.Object(ARRAY(x0, x1)), x5, x6, x7, x8)
Cond_Load3443(TRUE, java.lang.Object(ARRAY(x0, x1)), x0, x2, x3, java.lang.Object(ARRAY(x0, x1)), x4, x3, java.lang.Object(ARRAY(x0, x1)))

(8) DuplicateArgsRemoverProof (EQUIVALENT transformation)

Some arguments are removed because they only appear as duplicates.
We removed arguments according to the following replacements:

Cond_Load3443(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_Load3443(x1, x3, x4, x7, x8, x9)
Load3657(x1, x2, x3, x4, x5, x6, x7, x8) → Load3657(x2, x3, x6, x7, x8)
Cond_Load3443ARR2(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13) → Cond_Load3443ARR2(x1, x3, x4, x7, x8, x9, x10, x11, x12, x13)
Load3443ARR2(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12) → Load3443ARR2(x2, x3, x6, x7, x8, x9, x10, x11, x12)
Cond_Load3443ARR1(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11) → Cond_Load3443ARR1(x1, x3, x4, x7, x8, x9, x10, x11)
Load3443ARR1(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10) → Load3443ARR1(x2, x3, x6, x7, x8, x9, x10)
Load3443(x1, x2, x3, x4, x5, x6, x7, x8) → Load3443(x2, x3, x6, x7, x8)

(9) Obligation:

ITRS problem:

The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

(10) ITRStoIDPProof (EQUIVALENT transformation)

Added dependency pairs

(11) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

The ITRS R consists of the following rules:
Load2339(java.lang.Object(ARRAY(i303, a2291data)), i303, i304) → Cond_Load2339(i304 > 0 && i304 < i303, java.lang.Object(ARRAY(i303, a2291data)), i303, i304)
Cond_Load2339(TRUE, java.lang.Object(ARRAY(i303, a2291data)), i303, i304) → Load3443(i303, i304, 0, i303 - i304, java.lang.Object(ARRAY(i303, a2291data)))
Load3657(i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data))) → Load3443(i663, i304, i661 + 1, i662, java.lang.Object(ARRAY(i663, a3434data)))
Load3443(i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data))) → Load3443ARR1(i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data)), i706, i677)
Load3443ARR1(i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data)), i706, i677) → Cond_Load3443ARR1(i677 <= i706 && i661 + 1 > 0 && i661 + 1 < i663 && i661 >= 0 && i661 < i663 && i661 < i662 && i661 + 1 > 0, i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data)), i706, i677)
Cond_Load3443ARR1(TRUE, i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data)), i706, i677) → Load3443(i663, i304, i661 + 1, i662, java.lang.Object(ARRAY(i663, a3434data)))
Load3443(i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data))) → Load3443ARR2(i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data)), i977, i790, i706, i677)
Load3443ARR2(i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data)), i977, i790, i706, i677) → Cond_Load3443ARR2(i661 + 1 > 0 && i661 + 1 < i663 && i661 >= 0 && i661 < i663 && i661 + 1 > 0 && i661 + 1 < i663 && i677 > i706 && i661 + 1 > 0 && i661 + 1 < i663 && i661 < i662, i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data)), i977, i790, i706, i677)
Cond_Load3443ARR2(TRUE, i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data)), i977, i790, i706, i677) → Load3657(i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434dataNew)))
Load3443(i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data))) → Cond_Load3443(i661 >= i662 && i304 > 0 && i304 + 1 > 0, i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data)))
Cond_Load3443(TRUE, i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data))) → Load2339(java.lang.Object(ARRAY(i663, a3434data)), i663, i304 + 1)

The integer pair graph contains the following rules and edges:
(0): LOAD2339(java.lang.Object(ARRAY(i303[0], a2291data[0])), i303[0], i304[0]) → COND_LOAD2339(i304[0] > 0 && i304[0] < i303[0], java.lang.Object(ARRAY(i303[0], a2291data[0])), i303[0], i304[0])
(1): COND_LOAD2339(TRUE, java.lang.Object(ARRAY(i303[1], a2291data[1])), i303[1], i304[1]) → LOAD3443(i303[1], i304[1], 0, i303[1] - i304[1], java.lang.Object(ARRAY(i303[1], a2291data[1])))
(2): LOAD3657(i663[2], i304[2], i661[2], i662[2], java.lang.Object(ARRAY(i663[2], a3434data[2]))) → LOAD3443(i663[2], i304[2], i661[2] + 1, i662[2], java.lang.Object(ARRAY(i663[2], a3434data[2])))
(3): LOAD3443(i663[3], i304[3], i661[3], i662[3], java.lang.Object(ARRAY(i663[3], a3434data[3]))) → LOAD3443ARR1(i663[3], i304[3], i661[3], i662[3], java.lang.Object(ARRAY(i663[3], a3434data[3])), i706[3], i677[3])
(4): LOAD3443ARR1(i663[4], i304[4], i661[4], i662[4], java.lang.Object(ARRAY(i663[4], a3434data[4])), i706[4], i677[4]) → COND_LOAD3443ARR1(i677[4] <= i706[4] && i661[4] + 1 > 0 && i661[4] + 1 < i663[4] && i661[4] >= 0 && i661[4] < i663[4] && i661[4] < i662[4] && i661[4] + 1 > 0, i663[4], i304[4], i661[4], i662[4], java.lang.Object(ARRAY(i663[4], a3434data[4])), i706[4], i677[4])
(5): COND_LOAD3443ARR1(TRUE, i663[5], i304[5], i661[5], i662[5], java.lang.Object(ARRAY(i663[5], a3434data[5])), i706[5], i677[5]) → LOAD3443(i663[5], i304[5], i661[5] + 1, i662[5], java.lang.Object(ARRAY(i663[5], a3434data[5])))
(6): LOAD3443(i663[6], i304[6], i661[6], i662[6], java.lang.Object(ARRAY(i663[6], a3434data[6]))) → LOAD3443ARR2(i663[6], i304[6], i661[6], i662[6], java.lang.Object(ARRAY(i663[6], a3434data[6])), i977[6], i790[6], i706[6], i677[6])
(7): LOAD3443ARR2(i663[7], i304[7], i661[7], i662[7], java.lang.Object(ARRAY(i663[7], a3434data[7])), i977[7], i790[7], i706[7], i677[7]) → COND_LOAD3443ARR2(i661[7] + 1 > 0 && i661[7] + 1 < i663[7] && i661[7] >= 0 && i661[7] < i663[7] && i661[7] + 1 > 0 && i661[7] + 1 < i663[7] && i677[7] > i706[7] && i661[7] + 1 > 0 && i661[7] + 1 < i663[7] && i661[7] < i662[7], i663[7], i304[7], i661[7], i662[7], java.lang.Object(ARRAY(i663[7], a3434data[7])), i977[7], i790[7], i706[7], i677[7])
(8): COND_LOAD3443ARR2(TRUE, i663[8], i304[8], i661[8], i662[8], java.lang.Object(ARRAY(i663[8], a3434data[8])), i977[8], i790[8], i706[8], i677[8]) → LOAD3657(i663[8], i304[8], i661[8], i662[8], java.lang.Object(ARRAY(i663[8], a3434dataNew[8])))
(9): LOAD3443(i663[9], i304[9], i661[9], i662[9], java.lang.Object(ARRAY(i663[9], a3434data[9]))) → COND_LOAD3443(i661[9] >= i662[9] && i304[9] > 0 && i304[9] + 1 > 0, i663[9], i304[9], i661[9], i662[9], java.lang.Object(ARRAY(i663[9], a3434data[9])))
(10): COND_LOAD3443(TRUE, i663[10], i304[10], i661[10], i662[10], java.lang.Object(ARRAY(i663[10], a3434data[10]))) → LOAD2339(java.lang.Object(ARRAY(i663[10], a3434data[10])), i663[10], i304[10] + 1)

(0) -> (1), if ((i303[0] →^* i303[1])∧(i304[0] > 0 && i304[0] < i303[0] →^* TRUE)∧(java.lang.Object(ARRAY(i303[0], a2291data[0])) →^* java.lang.Object(ARRAY(i303[1], a2291data[1])))∧(i304[0] →^* i304[1]))

(1) -> (3), if ((i303[1] - i304[1] →^* i662[3])∧(i304[1] →^* i304[3])∧(i303[1] →^* i663[3])∧(java.lang.Object(ARRAY(i303[1], a2291data[1])) →^* java.lang.Object(ARRAY(i663[3], a3434data[3])))∧(0 →^* i661[3]))

(1) -> (6), if ((i303[1] - i304[1] →^* i662[6])∧(i304[1] →^* i304[6])∧(i303[1] →^* i663[6])∧(0 →^* i661[6])∧(java.lang.Object(ARRAY(i303[1], a2291data[1])) →^* java.lang.Object(ARRAY(i663[6], a3434data[6]))))

(1) -> (9), if ((i304[1] →^* i304[9])∧(0 →^* i661[9])∧(java.lang.Object(ARRAY(i303[1], a2291data[1])) →^* java.lang.Object(ARRAY(i663[9], a3434data[9])))∧(i303[1] →^* i663[9])∧(i303[1] - i304[1] →^* i662[9]))

(2) -> (3), if ((i304[2] →^* i304[3])∧(i662[2] →^* i662[3])∧(i663[2] →^* i663[3])∧(java.lang.Object(ARRAY(i663[2], a3434data[2])) →^* java.lang.Object(ARRAY(i663[3], a3434data[3])))∧(i661[2] + 1 →^* i661[3]))

(2) -> (6), if ((i304[2] →^* i304[6])∧(i663[2] →^* i663[6])∧(i661[2] + 1 →^* i661[6])∧(i662[2] →^* i662[6])∧(java.lang.Object(ARRAY(i663[2], a3434data[2])) →^* java.lang.Object(ARRAY(i663[6], a3434data[6]))))

(2) -> (9), if ((i662[2] →^* i662[9])∧(i661[2] + 1 →^* i661[9])∧(i304[2] →^* i304[9])∧(i663[2] →^* i663[9])∧(java.lang.Object(ARRAY(i663[2], a3434data[2])) →^* java.lang.Object(ARRAY(i663[9], a3434data[9]))))

(3) -> (4), if ((i706[3] →^* i706[4])∧(java.lang.Object(ARRAY(i663[3], a3434data[3])) →^* java.lang.Object(ARRAY(i663[4], a3434data[4])))∧(i663[3] →^* i663[4])∧(i304[3] →^* i304[4])∧(i662[3] →^* i662[4])∧(i661[3] →^* i661[4])∧(i677[3] →^* i677[4]))

(4) -> (5), if ((i304[4] →^* i304[5])∧(i677[4] <= i706[4] && i661[4] + 1 > 0 && i661[4] + 1 < i663[4] && i661[4] >= 0 && i661[4] < i663[4] && i661[4] < i662[4] && i661[4] + 1 > 0 →^* TRUE)∧(i661[4] →^* i661[5])∧(i677[4] →^* i677[5])∧(i706[4] →^* i706[5])∧(java.lang.Object(ARRAY(i663[4], a3434data[4])) →^* java.lang.Object(ARRAY(i663[5], a3434data[5])))∧(i662[4] →^* i662[5])∧(i663[4] →^* i663[5]))

(5) -> (3), if ((i661[5] + 1 →^* i661[3])∧(java.lang.Object(ARRAY(i663[5], a3434data[5])) →^* java.lang.Object(ARRAY(i663[3], a3434data[3])))∧(i662[5] →^* i662[3])∧(i663[5] →^* i663[3])∧(i304[5] →^* i304[3]))

(5) -> (6), if ((i661[5] + 1 →^* i661[6])∧(i304[5] →^* i304[6])∧(i662[5] →^* i662[6])∧(java.lang.Object(ARRAY(i663[5], a3434data[5])) →^* java.lang.Object(ARRAY(i663[6], a3434data[6])))∧(i663[5] →^* i663[6]))

(5) -> (9), if ((i661[5] + 1 →^* i661[9])∧(i663[5] →^* i663[9])∧(i304[5] →^* i304[9])∧(i662[5] →^* i662[9])∧(java.lang.Object(ARRAY(i663[5], a3434data[5])) →^* java.lang.Object(ARRAY(i663[9], a3434data[9]))))

(6) -> (7), if ((i706[6] →^* i706[7])∧(i790[6] →^* i790[7])∧(i677[6] →^* i677[7])∧(i661[6] →^* i661[7])∧(i304[6] →^* i304[7])∧(i662[6] →^* i662[7])∧(i663[6] →^* i663[7])∧(java.lang.Object(ARRAY(i663[6], a3434data[6])) →^* java.lang.Object(ARRAY(i663[7], a3434data[7])))∧(i977[6] →^* i977[7]))

(7) -> (8), if ((i304[7] →^* i304[8])∧(i663[7] →^* i663[8])∧(i662[7] →^* i662[8])∧(i706[7] →^* i706[8])∧(i977[7] →^* i977[8])∧(i661[7] + 1 > 0 && i661[7] + 1 < i663[7] && i661[7] >= 0 && i661[7] < i663[7] && i661[7] + 1 > 0 && i661[7] + 1 < i663[7] && i677[7] > i706[7] && i661[7] + 1 > 0 && i661[7] + 1 < i663[7] && i661[7] < i662[7] →^* TRUE)∧(i790[7] →^* i790[8])∧(java.lang.Object(ARRAY(i663[7], a3434data[7])) →^* java.lang.Object(ARRAY(i663[8], a3434data[8])))∧(i661[7] →^* i661[8])∧(i677[7] →^* i677[8]))

(8) -> (2), if ((i663[8] →^* i663[2])∧(i661[8] →^* i661[2])∧(i304[8] →^* i304[2])∧(i662[8] →^* i662[2])∧(java.lang.Object(ARRAY(i663[8], a3434dataNew[8])) →^* java.lang.Object(ARRAY(i663[2], a3434data[2]))))

(9) -> (10), if ((i304[9] →^* i304[10])∧(i663[9] →^* i663[10])∧(java.lang.Object(ARRAY(i663[9], a3434data[9])) →^* java.lang.Object(ARRAY(i663[10], a3434data[10])))∧(i661[9] >= i662[9] && i304[9] > 0 && i304[9] + 1 > 0 →^* TRUE)∧(i661[9] →^* i661[10])∧(i662[9] →^* i662[10]))

(10) -> (0), if ((i304[10] + 1 →^* i304[0])∧(i663[10] →^* i303[0])∧(java.lang.Object(ARRAY(i663[10], a3434data[10])) →^* java.lang.Object(ARRAY(i303[0], a2291data[0]))))

The set Q consists of the following terms:
Load2339(java.lang.Object(ARRAY(x0, x1)), x0, x2)
Cond_Load2339(TRUE, java.lang.Object(ARRAY(x0, x1)), x0, x2)
Load3657(x0, x1, x2, x3, java.lang.Object(ARRAY(x0, x4)))
Load3443(x0, x1, x2, x3, java.lang.Object(ARRAY(x0, x4)))
Load3443ARR1(x0, x1, x2, x3, java.lang.Object(ARRAY(x0, x4)), x5, x6)
Cond_Load3443ARR1(TRUE, x0, x1, x2, x3, java.lang.Object(ARRAY(x0, x4)), x5, x6)
Load3443ARR2(x0, x1, x2, x3, java.lang.Object(ARRAY(x0, x4)), x5, x6, x7, x8)
Cond_Load3443ARR2(TRUE, x0, x1, x2, x3, java.lang.Object(ARRAY(x0, x4)), x5, x6, x7, x8)
Cond_Load3443(TRUE, x0, x1, x2, x3, java.lang.Object(ARRAY(x0, x4)))

(12) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(13) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD2339(java.lang.Object(ARRAY(i303[0], a2291data[0])), i303[0], i304[0]) → COND_LOAD2339(i304[0] > 0 && i304[0] < i303[0], java.lang.Object(ARRAY(i303[0], a2291data[0])), i303[0], i304[0])
(1): COND_LOAD2339(TRUE, java.lang.Object(ARRAY(i303[1], a2291data[1])), i303[1], i304[1]) → LOAD3443(i303[1], i304[1], 0, i303[1] - i304[1], java.lang.Object(ARRAY(i303[1], a2291data[1])))
(2): LOAD3657(i663[2], i304[2], i661[2], i662[2], java.lang.Object(ARRAY(i663[2], a3434data[2]))) → LOAD3443(i663[2], i304[2], i661[2] + 1, i662[2], java.lang.Object(ARRAY(i663[2], a3434data[2])))
(3): LOAD3443(i663[3], i304[3], i661[3], i662[3], java.lang.Object(ARRAY(i663[3], a3434data[3]))) → LOAD3443ARR1(i663[3], i304[3], i661[3], i662[3], java.lang.Object(ARRAY(i663[3], a3434data[3])), i706[3], i677[3])
(4): LOAD3443ARR1(i663[4], i304[4], i661[4], i662[4], java.lang.Object(ARRAY(i663[4], a3434data[4])), i706[4], i677[4]) → COND_LOAD3443ARR1(i677[4] <= i706[4] && i661[4] + 1 > 0 && i661[4] + 1 < i663[4] && i661[4] >= 0 && i661[4] < i663[4] && i661[4] < i662[4] && i661[4] + 1 > 0, i663[4], i304[4], i661[4], i662[4], java.lang.Object(ARRAY(i663[4], a3434data[4])), i706[4], i677[4])
(5): COND_LOAD3443ARR1(TRUE, i663[5], i304[5], i661[5], i662[5], java.lang.Object(ARRAY(i663[5], a3434data[5])), i706[5], i677[5]) → LOAD3443(i663[5], i304[5], i661[5] + 1, i662[5], java.lang.Object(ARRAY(i663[5], a3434data[5])))
(6): LOAD3443(i663[6], i304[6], i661[6], i662[6], java.lang.Object(ARRAY(i663[6], a3434data[6]))) → LOAD3443ARR2(i663[6], i304[6], i661[6], i662[6], java.lang.Object(ARRAY(i663[6], a3434data[6])), i977[6], i790[6], i706[6], i677[6])
(7): LOAD3443ARR2(i663[7], i304[7], i661[7], i662[7], java.lang.Object(ARRAY(i663[7], a3434data[7])), i977[7], i790[7], i706[7], i677[7]) → COND_LOAD3443ARR2(i661[7] + 1 > 0 && i661[7] + 1 < i663[7] && i661[7] >= 0 && i661[7] < i663[7] && i661[7] + 1 > 0 && i661[7] + 1 < i663[7] && i677[7] > i706[7] && i661[7] + 1 > 0 && i661[7] + 1 < i663[7] && i661[7] < i662[7], i663[7], i304[7], i661[7], i662[7], java.lang.Object(ARRAY(i663[7], a3434data[7])), i977[7], i790[7], i706[7], i677[7])
(8): COND_LOAD3443ARR2(TRUE, i663[8], i304[8], i661[8], i662[8], java.lang.Object(ARRAY(i663[8], a3434data[8])), i977[8], i790[8], i706[8], i677[8]) → LOAD3657(i663[8], i304[8], i661[8], i662[8], java.lang.Object(ARRAY(i663[8], a3434dataNew[8])))
(9): LOAD3443(i663[9], i304[9], i661[9], i662[9], java.lang.Object(ARRAY(i663[9], a3434data[9]))) → COND_LOAD3443(i661[9] >= i662[9] && i304[9] > 0 && i304[9] + 1 > 0, i663[9], i304[9], i661[9], i662[9], java.lang.Object(ARRAY(i663[9], a3434data[9])))
(10): COND_LOAD3443(TRUE, i663[10], i304[10], i661[10], i662[10], java.lang.Object(ARRAY(i663[10], a3434data[10]))) → LOAD2339(java.lang.Object(ARRAY(i663[10], a3434data[10])), i663[10], i304[10] + 1)

(10) -> (0), if ((i304[10] + 1 →^* i304[0])∧(i663[10] →^* i303[0])∧(java.lang.Object(ARRAY(i663[10], a3434data[10])) →^* java.lang.Object(ARRAY(i303[0], a2291data[0]))))

(14) ItpfGraphProof (EQUIVALENT transformation)

Applied rule ItpfICap [ICap]

(15) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean

The following domains are used:

Boolean, Integer

(0) -> (1), if ((i303[0] →^* i303[1])∧(i304[0] > 0 && i304[0] < i303[0] →^* TRUE)∧((i303[0] →^* i303[1])∧(a2291data[0] →^* a2291data[1]))∧(i304[0] →^* i304[1]))

(1) -> (3), if ((i303[1] - i304[1] →^* i662[3])∧(i304[1] →^* i304[3])∧(i303[1] →^* i663[3])∧((i303[1] →^* i663[3])∧(a2291data[1] →^* a3434data[3]))∧(0 →^* i661[3]))

(1) -> (6), if ((i303[1] - i304[1] →^* i662[6])∧(i304[1] →^* i304[6])∧(i303[1] →^* i663[6])∧(0 →^* i661[6])∧((i303[1] →^* i663[6])∧(a2291data[1] →^* a3434data[6])))

(1) -> (9), if ((i304[1] →^* i304[9])∧(0 →^* i661[9])∧((i303[1] →^* i663[9])∧(a2291data[1] →^* a3434data[9]))∧(i303[1] →^* i663[9])∧(i303[1] - i304[1] →^* i662[9]))

(2) -> (3), if ((i304[2] →^* i304[3])∧(i662[2] →^* i662[3])∧(i663[2] →^* i663[3])∧((i663[2] →^* i663[3])∧(a3434data[2] →^* a3434data[3]))∧(i661[2] + 1 →^* i661[3]))

(2) -> (6), if ((i304[2] →^* i304[6])∧(i663[2] →^* i663[6])∧(i661[2] + 1 →^* i661[6])∧(i662[2] →^* i662[6])∧((i663[2] →^* i663[6])∧(a3434data[2] →^* a3434data[6])))

(2) -> (9), if ((i662[2] →^* i662[9])∧(i661[2] + 1 →^* i661[9])∧(i304[2] →^* i304[9])∧(i663[2] →^* i663[9])∧((i663[2] →^* i663[9])∧(a3434data[2] →^* a3434data[9])))

(3) -> (4), if ((i706[3] →^* i706[4])∧((i663[3] →^* i663[4])∧(a3434data[3] →^* a3434data[4]))∧(i663[3] →^* i663[4])∧(i304[3] →^* i304[4])∧(i662[3] →^* i662[4])∧(i661[3] →^* i661[4])∧(i677[3] →^* i677[4]))

(4) -> (5), if ((i304[4] →^* i304[5])∧(i677[4] <= i706[4] && i661[4] + 1 > 0 && i661[4] + 1 < i663[4] && i661[4] >= 0 && i661[4] < i663[4] && i661[4] < i662[4] && i661[4] + 1 > 0 →^* TRUE)∧(i661[4] →^* i661[5])∧(i677[4] →^* i677[5])∧(i706[4] →^* i706[5])∧((i663[4] →^* i663[5])∧(a3434data[4] →^* a3434data[5]))∧(i662[4] →^* i662[5])∧(i663[4] →^* i663[5]))

(5) -> (3), if ((i661[5] + 1 →^* i661[3])∧((i663[5] →^* i663[3])∧(a3434data[5] →^* a3434data[3]))∧(i662[5] →^* i662[3])∧(i663[5] →^* i663[3])∧(i304[5] →^* i304[3]))

(5) -> (6), if ((i661[5] + 1 →^* i661[6])∧(i304[5] →^* i304[6])∧(i662[5] →^* i662[6])∧((i663[5] →^* i663[6])∧(a3434data[5] →^* a3434data[6]))∧(i663[5] →^* i663[6]))

(5) -> (9), if ((i661[5] + 1 →^* i661[9])∧(i663[5] →^* i663[9])∧(i304[5] →^* i304[9])∧(i662[5] →^* i662[9])∧((i663[5] →^* i663[9])∧(a3434data[5] →^* a3434data[9])))

(6) -> (7), if ((i706[6] →^* i706[7])∧(i790[6] →^* i790[7])∧(i677[6] →^* i677[7])∧(i661[6] →^* i661[7])∧(i304[6] →^* i304[7])∧(i662[6] →^* i662[7])∧(i663[6] →^* i663[7])∧((i663[6] →^* i663[7])∧(a3434data[6] →^* a3434data[7]))∧(i977[6] →^* i977[7]))

(7) -> (8), if ((i304[7] →^* i304[8])∧(i663[7] →^* i663[8])∧(i662[7] →^* i662[8])∧(i706[7] →^* i706[8])∧(i977[7] →^* i977[8])∧(i661[7] + 1 > 0 && i661[7] + 1 < i663[7] && i661[7] >= 0 && i661[7] < i663[7] && i661[7] + 1 > 0 && i661[7] + 1 < i663[7] && i677[7] > i706[7] && i661[7] + 1 > 0 && i661[7] + 1 < i663[7] && i661[7] < i662[7] →^* TRUE)∧(i790[7] →^* i790[8])∧((i663[7] →^* i663[8])∧(a3434data[7] →^* a3434data[8]))∧(i661[7] →^* i661[8])∧(i677[7] →^* i677[8]))

(8) -> (2), if ((i663[8] →^* i663[2])∧(i661[8] →^* i661[2])∧(i304[8] →^* i304[2])∧(i662[8] →^* i662[2])∧((i663[8] →^* i663[2])∧(a3434dataNew[8] →^* a3434data[2])))

(9) -> (10), if ((i304[9] →^* i304[10])∧(i663[9] →^* i663[10])∧((i663[9] →^* i663[10])∧(a3434data[9] →^* a3434data[10]))∧(i661[9] >= i662[9] && i304[9] > 0 && i304[9] + 1 > 0 →^* TRUE)∧(i661[9] →^* i661[10])∧(i662[9] →^* i662[10]))

(10) -> (0), if ((i304[10] + 1 →^* i304[0])∧(i663[10] →^* i303[0])∧((i663[10] →^* i303[0])∧(a3434data[10] →^* a2291data[0])))

(16) IDPNonInfProof (SOUND transformation)

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.

For Pair LOAD2339(java.lang.Object(ARRAY(i303, a2291data)), i303, i304) → COND_LOAD2339(&&(>(i304, 0), <(i304, i303)), java.lang.Object(ARRAY(i303, a2291data)), i303, i304) the following chains were created:

We consider the chain LOAD2339(java.lang.Object(ARRAY(i303[0], a2291data[0])), i303[0], i304[0]) → COND_LOAD2339(&&(>(i304[0], 0), <(i304[0], i303[0])), java.lang.Object(ARRAY(i303[0], a2291data[0])), i303[0], i304[0]), COND_LOAD2339(TRUE, java.lang.Object(ARRAY(i303[1], a2291data[1])), i303[1], i304[1]) → LOAD3443(i303[1], i304[1], 0, -(i303[1], i304[1]), java.lang.Object(ARRAY(i303[1], a2291data[1]))) which results in the following constraint:
(1)    (i303[0]=i303[1]∧&&(>(i304[0], 0), <(i304[0], i303[0]))=TRUE∧a2291data[0]=a2291data[1]∧i304[0]=i304[1] ⇒ LOAD2339(java.lang.Object(ARRAY(i303[0], a2291data[0])), i303[0], i304[0])≥NonInfC∧LOAD2339(java.lang.Object(ARRAY(i303[0], a2291data[0])), i303[0], i304[0])≥COND_LOAD2339(&&(>(i304[0], 0), <(i304[0], i303[0])), java.lang.Object(ARRAY(i303[0], a2291data[0])), i303[0], i304[0])∧(U^Increasing(COND_LOAD2339(&&(>(i304[0], 0), <(i304[0], i303[0])), java.lang.Object(ARRAY(i303[0], a2291data[0])), i303[0], i304[0])), ≥))

We simplified constraint (1) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:
(2)    (>(i304[0], 0)=TRUE∧<(i304[0], i303[0])=TRUE ⇒ LOAD2339(java.lang.Object(ARRAY(i303[0], a2291data[0])), i303[0], i304[0])≥NonInfC∧LOAD2339(java.lang.Object(ARRAY(i303[0], a2291data[0])), i303[0], i304[0])≥COND_LOAD2339(&&(>(i304[0], 0), <(i304[0], i303[0])), java.lang.Object(ARRAY(i303[0], a2291data[0])), i303[0], i304[0])∧(U^Increasing(COND_LOAD2339(&&(>(i304[0], 0), <(i304[0], i303[0])), java.lang.Object(ARRAY(i303[0], a2291data[0])), i303[0], i304[0])), ≥))

We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(3)    (i304[0] + [-1] ≥ 0∧i303[0] + [-1] + [-1]i304[0] ≥ 0 ⇒ (U^Increasing(COND_LOAD2339(&&(>(i304[0], 0), <(i304[0], i303[0])), java.lang.Object(ARRAY(i303[0], a2291data[0])), i303[0], i304[0])), ≥)∧[(-1)Bound*bni_28] + [bni_28]i303[0] + [(-1)bni_28]i304[0] ≥ 0∧[(-1)bso_29] ≥ 0)

We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(4)    (i304[0] + [-1] ≥ 0∧i303[0] + [-1] + [-1]i304[0] ≥ 0 ⇒ (U^Increasing(COND_LOAD2339(&&(>(i304[0], 0), <(i304[0], i303[0])), java.lang.Object(ARRAY(i303[0], a2291data[0])), i303[0], i304[0])), ≥)∧[(-1)Bound*bni_28] + [bni_28]i303[0] + [(-1)bni_28]i304[0] ≥ 0∧[(-1)bso_29] ≥ 0)

We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(5)    (i304[0] + [-1] ≥ 0∧i303[0] + [-1] + [-1]i304[0] ≥ 0 ⇒ (U^Increasing(COND_LOAD2339(&&(>(i304[0], 0), <(i304[0], i303[0])), java.lang.Object(ARRAY(i303[0], a2291data[0])), i303[0], i304[0])), ≥)∧[(-1)Bound*bni_28] + [bni_28]i303[0] + [(-1)bni_28]i304[0] ≥ 0∧[(-1)bso_29] ≥ 0)

We simplified constraint (5) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(6)    (i304[0] + [-1] ≥ 0∧i303[0] + [-1] + [-1]i304[0] ≥ 0 ⇒ (U^Increasing(COND_LOAD2339(&&(>(i304[0], 0), <(i304[0], i303[0])), java.lang.Object(ARRAY(i303[0], a2291data[0])), i303[0], i304[0])), ≥)∧0 = 0∧[(-1)Bound*bni_28] + [bni_28]i303[0] + [(-1)bni_28]i304[0] ≥ 0∧0 = 0∧[(-1)bso_29] ≥ 0)

We simplified constraint (6) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(7)    (i304[0] ≥ 0∧i303[0] + [-2] + [-1]i304[0] ≥ 0 ⇒ (U^Increasing(COND_LOAD2339(&&(>(i304[0], 0), <(i304[0], i303[0])), java.lang.Object(ARRAY(i303[0], a2291data[0])), i303[0], i304[0])), ≥)∧0 = 0∧[(-1)Bound*bni_28 + (-1)bni_28] + [bni_28]i303[0] + [(-1)bni_28]i304[0] ≥ 0∧0 = 0∧[(-1)bso_29] ≥ 0)

We simplified constraint (7) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(8)    (i304[0] ≥ 0∧i303[0] ≥ 0 ⇒ (U^Increasing(COND_LOAD2339(&&(>(i304[0], 0), <(i304[0], i303[0])), java.lang.Object(ARRAY(i303[0], a2291data[0])), i303[0], i304[0])), ≥)∧0 = 0∧[(-1)Bound*bni_28 + bni_28] + [bni_28]i303[0] ≥ 0∧0 = 0∧[(-1)bso_29] ≥ 0)

For Pair COND_LOAD2339(TRUE, java.lang.Object(ARRAY(i303, a2291data)), i303, i304) → LOAD3443(i303, i304, 0, -(i303, i304), java.lang.Object(ARRAY(i303, a2291data))) the following chains were created:

We consider the chain COND_LOAD2339(TRUE, java.lang.Object(ARRAY(i303[1], a2291data[1])), i303[1], i304[1]) → LOAD3443(i303[1], i304[1], 0, -(i303[1], i304[1]), java.lang.Object(ARRAY(i303[1], a2291data[1]))) which results in the following constraint:
(9)    (COND_LOAD2339(TRUE, java.lang.Object(ARRAY(i303[1], a2291data[1])), i303[1], i304[1])≥NonInfC∧COND_LOAD2339(TRUE, java.lang.Object(ARRAY(i303[1], a2291data[1])), i303[1], i304[1])≥LOAD3443(i303[1], i304[1], 0, -(i303[1], i304[1]), java.lang.Object(ARRAY(i303[1], a2291data[1])))∧(U^Increasing(LOAD3443(i303[1], i304[1], 0, -(i303[1], i304[1]), java.lang.Object(ARRAY(i303[1], a2291data[1])))), ≥))

We simplified constraint (9) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(10)    ((U^Increasing(LOAD3443(i303[1], i304[1], 0, -(i303[1], i304[1]), java.lang.Object(ARRAY(i303[1], a2291data[1])))), ≥)∧[(-1)bso_31] ≥ 0)

We simplified constraint (10) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(11)    ((U^Increasing(LOAD3443(i303[1], i304[1], 0, -(i303[1], i304[1]), java.lang.Object(ARRAY(i303[1], a2291data[1])))), ≥)∧[(-1)bso_31] ≥ 0)

We simplified constraint (11) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(12)    ((U^Increasing(LOAD3443(i303[1], i304[1], 0, -(i303[1], i304[1]), java.lang.Object(ARRAY(i303[1], a2291data[1])))), ≥)∧[(-1)bso_31] ≥ 0)

We simplified constraint (12) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(13)    ((U^Increasing(LOAD3443(i303[1], i304[1], 0, -(i303[1], i304[1]), java.lang.Object(ARRAY(i303[1], a2291data[1])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_31] ≥ 0)

For Pair LOAD3657(i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data))) → LOAD3443(i663, i304, +(i661, 1), i662, java.lang.Object(ARRAY(i663, a3434data))) the following chains were created:

We consider the chain LOAD3657(i663[2], i304[2], i661[2], i662[2], java.lang.Object(ARRAY(i663[2], a3434data[2]))) → LOAD3443(i663[2], i304[2], +(i661[2], 1), i662[2], java.lang.Object(ARRAY(i663[2], a3434data[2]))) which results in the following constraint:
(14)    (LOAD3657(i663[2], i304[2], i661[2], i662[2], java.lang.Object(ARRAY(i663[2], a3434data[2])))≥NonInfC∧LOAD3657(i663[2], i304[2], i661[2], i662[2], java.lang.Object(ARRAY(i663[2], a3434data[2])))≥LOAD3443(i663[2], i304[2], +(i661[2], 1), i662[2], java.lang.Object(ARRAY(i663[2], a3434data[2])))∧(U^Increasing(LOAD3443(i663[2], i304[2], +(i661[2], 1), i662[2], java.lang.Object(ARRAY(i663[2], a3434data[2])))), ≥))

We simplified constraint (14) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(15)    ((U^Increasing(LOAD3443(i663[2], i304[2], +(i661[2], 1), i662[2], java.lang.Object(ARRAY(i663[2], a3434data[2])))), ≥)∧[(-1)bso_33] ≥ 0)

We simplified constraint (15) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(16)    ((U^Increasing(LOAD3443(i663[2], i304[2], +(i661[2], 1), i662[2], java.lang.Object(ARRAY(i663[2], a3434data[2])))), ≥)∧[(-1)bso_33] ≥ 0)

We simplified constraint (16) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(17)    ((U^Increasing(LOAD3443(i663[2], i304[2], +(i661[2], 1), i662[2], java.lang.Object(ARRAY(i663[2], a3434data[2])))), ≥)∧[(-1)bso_33] ≥ 0)

We simplified constraint (17) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(18)    ((U^Increasing(LOAD3443(i663[2], i304[2], +(i661[2], 1), i662[2], java.lang.Object(ARRAY(i663[2], a3434data[2])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_33] ≥ 0)

For Pair LOAD3443(i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data))) → LOAD3443ARR1(i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data)), i706, i677) the following chains were created:

We consider the chain LOAD3443(i663[3], i304[3], i661[3], i662[3], java.lang.Object(ARRAY(i663[3], a3434data[3]))) → LOAD3443ARR1(i663[3], i304[3], i661[3], i662[3], java.lang.Object(ARRAY(i663[3], a3434data[3])), i706[3], i677[3]) which results in the following constraint:
(19)    (LOAD3443(i663[3], i304[3], i661[3], i662[3], java.lang.Object(ARRAY(i663[3], a3434data[3])))≥NonInfC∧LOAD3443(i663[3], i304[3], i661[3], i662[3], java.lang.Object(ARRAY(i663[3], a3434data[3])))≥LOAD3443ARR1(i663[3], i304[3], i661[3], i662[3], java.lang.Object(ARRAY(i663[3], a3434data[3])), i706[3], i677[3])∧(U^Increasing(LOAD3443ARR1(i663[3], i304[3], i661[3], i662[3], java.lang.Object(ARRAY(i663[3], a3434data[3])), i706[3], i677[3])), ≥))

We simplified constraint (19) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(20)    ((U^Increasing(LOAD3443ARR1(i663[3], i304[3], i661[3], i662[3], java.lang.Object(ARRAY(i663[3], a3434data[3])), i706[3], i677[3])), ≥)∧[(-1)bso_35] ≥ 0)

We simplified constraint (20) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(21)    ((U^Increasing(LOAD3443ARR1(i663[3], i304[3], i661[3], i662[3], java.lang.Object(ARRAY(i663[3], a3434data[3])), i706[3], i677[3])), ≥)∧[(-1)bso_35] ≥ 0)

We simplified constraint (21) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(22)    ((U^Increasing(LOAD3443ARR1(i663[3], i304[3], i661[3], i662[3], java.lang.Object(ARRAY(i663[3], a3434data[3])), i706[3], i677[3])), ≥)∧[(-1)bso_35] ≥ 0)

We simplified constraint (22) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(23)    ((U^Increasing(LOAD3443ARR1(i663[3], i304[3], i661[3], i662[3], java.lang.Object(ARRAY(i663[3], a3434data[3])), i706[3], i677[3])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_35] ≥ 0)

For Pair LOAD3443ARR1(i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data)), i706, i677) → COND_LOAD3443ARR1(&&(&&(&&(&&(&&(&&(<=(i677, i706), >(+(i661, 1), 0)), <(+(i661, 1), i663)), >=(i661, 0)), <(i661, i663)), <(i661, i662)), >(+(i661, 1), 0)), i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data)), i706, i677) the following chains were created:

We consider the chain LOAD3443ARR1(i663[4], i304[4], i661[4], i662[4], java.lang.Object(ARRAY(i663[4], a3434data[4])), i706[4], i677[4]) → COND_LOAD3443ARR1(&&(&&(&&(&&(&&(&&(<=(i677[4], i706[4]), >(+(i661[4], 1), 0)), <(+(i661[4], 1), i663[4])), >=(i661[4], 0)), <(i661[4], i663[4])), <(i661[4], i662[4])), >(+(i661[4], 1), 0)), i663[4], i304[4], i661[4], i662[4], java.lang.Object(ARRAY(i663[4], a3434data[4])), i706[4], i677[4]), COND_LOAD3443ARR1(TRUE, i663[5], i304[5], i661[5], i662[5], java.lang.Object(ARRAY(i663[5], a3434data[5])), i706[5], i677[5]) → LOAD3443(i663[5], i304[5], +(i661[5], 1), i662[5], java.lang.Object(ARRAY(i663[5], a3434data[5]))) which results in the following constraint:
(24)    (i304[4]=i304[5]∧&&(&&(&&(&&(&&(&&(<=(i677[4], i706[4]), >(+(i661[4], 1), 0)), <(+(i661[4], 1), i663[4])), >=(i661[4], 0)), <(i661[4], i663[4])), <(i661[4], i662[4])), >(+(i661[4], 1), 0))=TRUE∧i661[4]=i661[5]∧i677[4]=i677[5]∧i706[4]=i706[5]∧i663[4]=i663[5]∧a3434data[4]=a3434data[5]∧i662[4]=i662[5] ⇒ LOAD3443ARR1(i663[4], i304[4], i661[4], i662[4], java.lang.Object(ARRAY(i663[4], a3434data[4])), i706[4], i677[4])≥NonInfC∧LOAD3443ARR1(i663[4], i304[4], i661[4], i662[4], java.lang.Object(ARRAY(i663[4], a3434data[4])), i706[4], i677[4])≥COND_LOAD3443ARR1(&&(&&(&&(&&(&&(&&(<=(i677[4], i706[4]), >(+(i661[4], 1), 0)), <(+(i661[4], 1), i663[4])), >=(i661[4], 0)), <(i661[4], i663[4])), <(i661[4], i662[4])), >(+(i661[4], 1), 0)), i663[4], i304[4], i661[4], i662[4], java.lang.Object(ARRAY(i663[4], a3434data[4])), i706[4], i677[4])∧(U^Increasing(COND_LOAD3443ARR1(&&(&&(&&(&&(&&(&&(<=(i677[4], i706[4]), >(+(i661[4], 1), 0)), <(+(i661[4], 1), i663[4])), >=(i661[4], 0)), <(i661[4], i663[4])), <(i661[4], i662[4])), >(+(i661[4], 1), 0)), i663[4], i304[4], i661[4], i662[4], java.lang.Object(ARRAY(i663[4], a3434data[4])), i706[4], i677[4])), ≥))

We simplified constraint (24) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:
(25)    (>(+(i661[4], 1), 0)=TRUE∧<(i661[4], i662[4])=TRUE∧<(i661[4], i663[4])=TRUE∧>=(i661[4], 0)=TRUE∧<(+(i661[4], 1), i663[4])=TRUE∧<=(i677[4], i706[4])=TRUE ⇒ LOAD3443ARR1(i663[4], i304[4], i661[4], i662[4], java.lang.Object(ARRAY(i663[4], a3434data[4])), i706[4], i677[4])≥NonInfC∧LOAD3443ARR1(i663[4], i304[4], i661[4], i662[4], java.lang.Object(ARRAY(i663[4], a3434data[4])), i706[4], i677[4])≥COND_LOAD3443ARR1(&&(&&(&&(&&(&&(&&(<=(i677[4], i706[4]), >(+(i661[4], 1), 0)), <(+(i661[4], 1), i663[4])), >=(i661[4], 0)), <(i661[4], i663[4])), <(i661[4], i662[4])), >(+(i661[4], 1), 0)), i663[4], i304[4], i661[4], i662[4], java.lang.Object(ARRAY(i663[4], a3434data[4])), i706[4], i677[4])∧(U^Increasing(COND_LOAD3443ARR1(&&(&&(&&(&&(&&(&&(<=(i677[4], i706[4]), >(+(i661[4], 1), 0)), <(+(i661[4], 1), i663[4])), >=(i661[4], 0)), <(i661[4], i663[4])), <(i661[4], i662[4])), >(+(i661[4], 1), 0)), i663[4], i304[4], i661[4], i662[4], java.lang.Object(ARRAY(i663[4], a3434data[4])), i706[4], i677[4])), ≥))

We simplified constraint (25) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(26)    (i661[4] ≥ 0∧i662[4] + [-1] + [-1]i661[4] ≥ 0∧i663[4] + [-1] + [-1]i661[4] ≥ 0∧i661[4] ≥ 0∧i663[4] + [-2] + [-1]i661[4] ≥ 0∧i706[4] + [-1]i677[4] ≥ 0 ⇒ (U^Increasing(COND_LOAD3443ARR1(&&(&&(&&(&&(&&(&&(<=(i677[4], i706[4]), >(+(i661[4], 1), 0)), <(+(i661[4], 1), i663[4])), >=(i661[4], 0)), <(i661[4], i663[4])), <(i661[4], i662[4])), >(+(i661[4], 1), 0)), i663[4], i304[4], i661[4], i662[4], java.lang.Object(ARRAY(i663[4], a3434data[4])), i706[4], i677[4])), ≥)∧[(-1)Bound*bni_36] + [bni_36]i663[4] + [(-1)bni_36]i304[4] ≥ 0∧[(-1)bso_37] ≥ 0)

We simplified constraint (26) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(27)    (i661[4] ≥ 0∧i662[4] + [-1] + [-1]i661[4] ≥ 0∧i663[4] + [-1] + [-1]i661[4] ≥ 0∧i661[4] ≥ 0∧i663[4] + [-2] + [-1]i661[4] ≥ 0∧i706[4] + [-1]i677[4] ≥ 0 ⇒ (U^Increasing(COND_LOAD3443ARR1(&&(&&(&&(&&(&&(&&(<=(i677[4], i706[4]), >(+(i661[4], 1), 0)), <(+(i661[4], 1), i663[4])), >=(i661[4], 0)), <(i661[4], i663[4])), <(i661[4], i662[4])), >(+(i661[4], 1), 0)), i663[4], i304[4], i661[4], i662[4], java.lang.Object(ARRAY(i663[4], a3434data[4])), i706[4], i677[4])), ≥)∧[(-1)Bound*bni_36] + [bni_36]i663[4] + [(-1)bni_36]i304[4] ≥ 0∧[(-1)bso_37] ≥ 0)

We simplified constraint (27) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(28)    (i661[4] ≥ 0∧i662[4] + [-1] + [-1]i661[4] ≥ 0∧i663[4] + [-1] + [-1]i661[4] ≥ 0∧i661[4] ≥ 0∧i663[4] + [-2] + [-1]i661[4] ≥ 0∧i706[4] + [-1]i677[4] ≥ 0 ⇒ (U^Increasing(COND_LOAD3443ARR1(&&(&&(&&(&&(&&(&&(<=(i677[4], i706[4]), >(+(i661[4], 1), 0)), <(+(i661[4], 1), i663[4])), >=(i661[4], 0)), <(i661[4], i663[4])), <(i661[4], i662[4])), >(+(i661[4], 1), 0)), i663[4], i304[4], i661[4], i662[4], java.lang.Object(ARRAY(i663[4], a3434data[4])), i706[4], i677[4])), ≥)∧[(-1)Bound*bni_36] + [bni_36]i663[4] + [(-1)bni_36]i304[4] ≥ 0∧[(-1)bso_37] ≥ 0)

We simplified constraint (28) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(29)    (i661[4] ≥ 0∧i662[4] + [-1] + [-1]i661[4] ≥ 0∧i663[4] + [-1] + [-1]i661[4] ≥ 0∧i661[4] ≥ 0∧i663[4] + [-2] + [-1]i661[4] ≥ 0∧i706[4] + [-1]i677[4] ≥ 0 ⇒ (U^Increasing(COND_LOAD3443ARR1(&&(&&(&&(&&(&&(&&(<=(i677[4], i706[4]), >(+(i661[4], 1), 0)), <(+(i661[4], 1), i663[4])), >=(i661[4], 0)), <(i661[4], i663[4])), <(i661[4], i662[4])), >(+(i661[4], 1), 0)), i663[4], i304[4], i661[4], i662[4], java.lang.Object(ARRAY(i663[4], a3434data[4])), i706[4], i677[4])), ≥)∧0 = 0∧[(-1)bni_36] = 0∧[(-1)Bound*bni_36] + [bni_36]i663[4] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_37] ≥ 0)

We simplified constraint (29) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(30)    (i661[4] ≥ 0∧i662[4] ≥ 0∧i663[4] + [-1] + [-1]i661[4] ≥ 0∧i661[4] ≥ 0∧i663[4] + [-2] + [-1]i661[4] ≥ 0∧i706[4] + [-1]i677[4] ≥ 0 ⇒ (U^Increasing(COND_LOAD3443ARR1(&&(&&(&&(&&(&&(&&(<=(i677[4], i706[4]), >(+(i661[4], 1), 0)), <(+(i661[4], 1), i663[4])), >=(i661[4], 0)), <(i661[4], i663[4])), <(i661[4], i662[4])), >(+(i661[4], 1), 0)), i663[4], i304[4], i661[4], i662[4], java.lang.Object(ARRAY(i663[4], a3434data[4])), i706[4], i677[4])), ≥)∧0 = 0∧[(-1)bni_36] = 0∧[(-1)Bound*bni_36] + [bni_36]i663[4] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_37] ≥ 0)

We simplified constraint (30) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(31)    (i661[4] ≥ 0∧i662[4] ≥ 0∧i663[4] ≥ 0∧i661[4] ≥ 0∧[-1] + i663[4] ≥ 0∧i706[4] + [-1]i677[4] ≥ 0 ⇒ (U^Increasing(COND_LOAD3443ARR1(&&(&&(&&(&&(&&(&&(<=(i677[4], i706[4]), >(+(i661[4], 1), 0)), <(+(i661[4], 1), i663[4])), >=(i661[4], 0)), <(i661[4], i663[4])), <(i661[4], i662[4])), >(+(i661[4], 1), 0)), i663[4], i304[4], i661[4], i662[4], java.lang.Object(ARRAY(i663[4], a3434data[4])), i706[4], i677[4])), ≥)∧0 = 0∧[(-1)bni_36] = 0∧[(-1)Bound*bni_36 + bni_36] + [bni_36]i661[4] + [bni_36]i663[4] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_37] ≥ 0)

We simplified constraint (31) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(32)    (i661[4] ≥ 0∧i662[4] ≥ 0∧[1] + i663[4] ≥ 0∧i661[4] ≥ 0∧i663[4] ≥ 0∧i706[4] + [-1]i677[4] ≥ 0 ⇒ (U^Increasing(COND_LOAD3443ARR1(&&(&&(&&(&&(&&(&&(<=(i677[4], i706[4]), >(+(i661[4], 1), 0)), <(+(i661[4], 1), i663[4])), >=(i661[4], 0)), <(i661[4], i663[4])), <(i661[4], i662[4])), >(+(i661[4], 1), 0)), i663[4], i304[4], i661[4], i662[4], java.lang.Object(ARRAY(i663[4], a3434data[4])), i706[4], i677[4])), ≥)∧0 = 0∧[(-1)bni_36] = 0∧[(-1)Bound*bni_36 + (2)bni_36] + [bni_36]i661[4] + [bni_36]i663[4] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_37] ≥ 0)

We simplified constraint (32) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(33)    (i661[4] ≥ 0∧i662[4] ≥ 0∧[1] + i663[4] ≥ 0∧i661[4] ≥ 0∧i663[4] ≥ 0∧i706[4] ≥ 0 ⇒ (U^Increasing(COND_LOAD3443ARR1(&&(&&(&&(&&(&&(&&(<=(i677[4], i706[4]), >(+(i661[4], 1), 0)), <(+(i661[4], 1), i663[4])), >=(i661[4], 0)), <(i661[4], i663[4])), <(i661[4], i662[4])), >(+(i661[4], 1), 0)), i663[4], i304[4], i661[4], i662[4], java.lang.Object(ARRAY(i663[4], a3434data[4])), i706[4], i677[4])), ≥)∧0 = 0∧[(-1)bni_36] = 0∧[(-1)Bound*bni_36 + (2)bni_36] + [bni_36]i661[4] + [bni_36]i663[4] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_37] ≥ 0)

We simplified constraint (33) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
(34)    (i661[4] ≥ 0∧i662[4] ≥ 0∧[1] + i663[4] ≥ 0∧i661[4] ≥ 0∧i663[4] ≥ 0∧i706[4] ≥ 0∧i677[4] ≥ 0 ⇒ (U^Increasing(COND_LOAD3443ARR1(&&(&&(&&(&&(&&(&&(<=(i677[4], i706[4]), >(+(i661[4], 1), 0)), <(+(i661[4], 1), i663[4])), >=(i661[4], 0)), <(i661[4], i663[4])), <(i661[4], i662[4])), >(+(i661[4], 1), 0)), i663[4], i304[4], i661[4], i662[4], java.lang.Object(ARRAY(i663[4], a3434data[4])), i706[4], i677[4])), ≥)∧0 = 0∧[(-1)bni_36] = 0∧[(-1)Bound*bni_36 + (2)bni_36] + [bni_36]i661[4] + [bni_36]i663[4] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_37] ≥ 0)

(35)    (i661[4] ≥ 0∧i662[4] ≥ 0∧[1] + i663[4] ≥ 0∧i661[4] ≥ 0∧i663[4] ≥ 0∧i706[4] ≥ 0∧i677[4] ≥ 0 ⇒ (U^Increasing(COND_LOAD3443ARR1(&&(&&(&&(&&(&&(&&(<=(i677[4], i706[4]), >(+(i661[4], 1), 0)), <(+(i661[4], 1), i663[4])), >=(i661[4], 0)), <(i661[4], i663[4])), <(i661[4], i662[4])), >(+(i661[4], 1), 0)), i663[4], i304[4], i661[4], i662[4], java.lang.Object(ARRAY(i663[4], a3434data[4])), i706[4], i677[4])), ≥)∧0 = 0∧[(-1)bni_36] = 0∧[(-1)Bound*bni_36 + (2)bni_36] + [bni_36]i661[4] + [bni_36]i663[4] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_37] ≥ 0)

For Pair COND_LOAD3443ARR1(TRUE, i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data)), i706, i677) → LOAD3443(i663, i304, +(i661, 1), i662, java.lang.Object(ARRAY(i663, a3434data))) the following chains were created:

We consider the chain COND_LOAD3443ARR1(TRUE, i663[5], i304[5], i661[5], i662[5], java.lang.Object(ARRAY(i663[5], a3434data[5])), i706[5], i677[5]) → LOAD3443(i663[5], i304[5], +(i661[5], 1), i662[5], java.lang.Object(ARRAY(i663[5], a3434data[5]))) which results in the following constraint:
(36)    (COND_LOAD3443ARR1(TRUE, i663[5], i304[5], i661[5], i662[5], java.lang.Object(ARRAY(i663[5], a3434data[5])), i706[5], i677[5])≥NonInfC∧COND_LOAD3443ARR1(TRUE, i663[5], i304[5], i661[5], i662[5], java.lang.Object(ARRAY(i663[5], a3434data[5])), i706[5], i677[5])≥LOAD3443(i663[5], i304[5], +(i661[5], 1), i662[5], java.lang.Object(ARRAY(i663[5], a3434data[5])))∧(U^Increasing(LOAD3443(i663[5], i304[5], +(i661[5], 1), i662[5], java.lang.Object(ARRAY(i663[5], a3434data[5])))), ≥))

We simplified constraint (36) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(37)    ((U^Increasing(LOAD3443(i663[5], i304[5], +(i661[5], 1), i662[5], java.lang.Object(ARRAY(i663[5], a3434data[5])))), ≥)∧[(-1)bso_39] ≥ 0)

We simplified constraint (37) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(38)    ((U^Increasing(LOAD3443(i663[5], i304[5], +(i661[5], 1), i662[5], java.lang.Object(ARRAY(i663[5], a3434data[5])))), ≥)∧[(-1)bso_39] ≥ 0)

We simplified constraint (38) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(39)    ((U^Increasing(LOAD3443(i663[5], i304[5], +(i661[5], 1), i662[5], java.lang.Object(ARRAY(i663[5], a3434data[5])))), ≥)∧[(-1)bso_39] ≥ 0)

We simplified constraint (39) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(40)    ((U^Increasing(LOAD3443(i663[5], i304[5], +(i661[5], 1), i662[5], java.lang.Object(ARRAY(i663[5], a3434data[5])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_39] ≥ 0)

For Pair LOAD3443(i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data))) → LOAD3443ARR2(i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data)), i977, i790, i706, i677) the following chains were created:

We consider the chain LOAD3443(i663[6], i304[6], i661[6], i662[6], java.lang.Object(ARRAY(i663[6], a3434data[6]))) → LOAD3443ARR2(i663[6], i304[6], i661[6], i662[6], java.lang.Object(ARRAY(i663[6], a3434data[6])), i977[6], i790[6], i706[6], i677[6]) which results in the following constraint:
(41)    (LOAD3443(i663[6], i304[6], i661[6], i662[6], java.lang.Object(ARRAY(i663[6], a3434data[6])))≥NonInfC∧LOAD3443(i663[6], i304[6], i661[6], i662[6], java.lang.Object(ARRAY(i663[6], a3434data[6])))≥LOAD3443ARR2(i663[6], i304[6], i661[6], i662[6], java.lang.Object(ARRAY(i663[6], a3434data[6])), i977[6], i790[6], i706[6], i677[6])∧(U^Increasing(LOAD3443ARR2(i663[6], i304[6], i661[6], i662[6], java.lang.Object(ARRAY(i663[6], a3434data[6])), i977[6], i790[6], i706[6], i677[6])), ≥))

We simplified constraint (41) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(42)    ((U^Increasing(LOAD3443ARR2(i663[6], i304[6], i661[6], i662[6], java.lang.Object(ARRAY(i663[6], a3434data[6])), i977[6], i790[6], i706[6], i677[6])), ≥)∧[(-1)bso_41] ≥ 0)

We simplified constraint (42) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(43)    ((U^Increasing(LOAD3443ARR2(i663[6], i304[6], i661[6], i662[6], java.lang.Object(ARRAY(i663[6], a3434data[6])), i977[6], i790[6], i706[6], i677[6])), ≥)∧[(-1)bso_41] ≥ 0)

We simplified constraint (43) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(44)    ((U^Increasing(LOAD3443ARR2(i663[6], i304[6], i661[6], i662[6], java.lang.Object(ARRAY(i663[6], a3434data[6])), i977[6], i790[6], i706[6], i677[6])), ≥)∧[(-1)bso_41] ≥ 0)

We simplified constraint (44) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(45)    ((U^Increasing(LOAD3443ARR2(i663[6], i304[6], i661[6], i662[6], java.lang.Object(ARRAY(i663[6], a3434data[6])), i977[6], i790[6], i706[6], i677[6])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_41] ≥ 0)

For Pair LOAD3443ARR2(i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data)), i977, i790, i706, i677) → COND_LOAD3443ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i661, 1), 0), <(+(i661, 1), i663)), >=(i661, 0)), <(i661, i663)), >(+(i661, 1), 0)), <(+(i661, 1), i663)), >(i677, i706)), >(+(i661, 1), 0)), <(+(i661, 1), i663)), <(i661, i662)), i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data)), i977, i790, i706, i677) the following chains were created:

We consider the chain LOAD3443ARR2(i663[7], i304[7], i661[7], i662[7], java.lang.Object(ARRAY(i663[7], a3434data[7])), i977[7], i790[7], i706[7], i677[7]) → COND_LOAD3443ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i661[7], 1), 0), <(+(i661[7], 1), i663[7])), >=(i661[7], 0)), <(i661[7], i663[7])), >(+(i661[7], 1), 0)), <(+(i661[7], 1), i663[7])), >(i677[7], i706[7])), >(+(i661[7], 1), 0)), <(+(i661[7], 1), i663[7])), <(i661[7], i662[7])), i663[7], i304[7], i661[7], i662[7], java.lang.Object(ARRAY(i663[7], a3434data[7])), i977[7], i790[7], i706[7], i677[7]), COND_LOAD3443ARR2(TRUE, i663[8], i304[8], i661[8], i662[8], java.lang.Object(ARRAY(i663[8], a3434data[8])), i977[8], i790[8], i706[8], i677[8]) → LOAD3657(i663[8], i304[8], i661[8], i662[8], java.lang.Object(ARRAY(i663[8], a3434dataNew[8]))) which results in the following constraint:
(46)    (i304[7]=i304[8]∧i663[7]=i663[8]∧i662[7]=i662[8]∧i706[7]=i706[8]∧i977[7]=i977[8]∧&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i661[7], 1), 0), <(+(i661[7], 1), i663[7])), >=(i661[7], 0)), <(i661[7], i663[7])), >(+(i661[7], 1), 0)), <(+(i661[7], 1), i663[7])), >(i677[7], i706[7])), >(+(i661[7], 1), 0)), <(+(i661[7], 1), i663[7])), <(i661[7], i662[7]))=TRUE∧i790[7]=i790[8]∧a3434data[7]=a3434data[8]∧i661[7]=i661[8]∧i677[7]=i677[8] ⇒ LOAD3443ARR2(i663[7], i304[7], i661[7], i662[7], java.lang.Object(ARRAY(i663[7], a3434data[7])), i977[7], i790[7], i706[7], i677[7])≥NonInfC∧LOAD3443ARR2(i663[7], i304[7], i661[7], i662[7], java.lang.Object(ARRAY(i663[7], a3434data[7])), i977[7], i790[7], i706[7], i677[7])≥COND_LOAD3443ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i661[7], 1), 0), <(+(i661[7], 1), i663[7])), >=(i661[7], 0)), <(i661[7], i663[7])), >(+(i661[7], 1), 0)), <(+(i661[7], 1), i663[7])), >(i677[7], i706[7])), >(+(i661[7], 1), 0)), <(+(i661[7], 1), i663[7])), <(i661[7], i662[7])), i663[7], i304[7], i661[7], i662[7], java.lang.Object(ARRAY(i663[7], a3434data[7])), i977[7], i790[7], i706[7], i677[7])∧(U^Increasing(COND_LOAD3443ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i661[7], 1), 0), <(+(i661[7], 1), i663[7])), >=(i661[7], 0)), <(i661[7], i663[7])), >(+(i661[7], 1), 0)), <(+(i661[7], 1), i663[7])), >(i677[7], i706[7])), >(+(i661[7], 1), 0)), <(+(i661[7], 1), i663[7])), <(i661[7], i662[7])), i663[7], i304[7], i661[7], i662[7], java.lang.Object(ARRAY(i663[7], a3434data[7])), i977[7], i790[7], i706[7], i677[7])), ≥))

We simplified constraint (46) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:
(47)    (<(i661[7], i662[7])=TRUE∧<(+(i661[7], 1), i663[7])=TRUE∧>(+(i661[7], 1), 0)=TRUE∧>(i677[7], i706[7])=TRUE∧<(i661[7], i663[7])=TRUE∧>=(i661[7], 0)=TRUE ⇒ LOAD3443ARR2(i663[7], i304[7], i661[7], i662[7], java.lang.Object(ARRAY(i663[7], a3434data[7])), i977[7], i790[7], i706[7], i677[7])≥NonInfC∧LOAD3443ARR2(i663[7], i304[7], i661[7], i662[7], java.lang.Object(ARRAY(i663[7], a3434data[7])), i977[7], i790[7], i706[7], i677[7])≥COND_LOAD3443ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i661[7], 1), 0), <(+(i661[7], 1), i663[7])), >=(i661[7], 0)), <(i661[7], i663[7])), >(+(i661[7], 1), 0)), <(+(i661[7], 1), i663[7])), >(i677[7], i706[7])), >(+(i661[7], 1), 0)), <(+(i661[7], 1), i663[7])), <(i661[7], i662[7])), i663[7], i304[7], i661[7], i662[7], java.lang.Object(ARRAY(i663[7], a3434data[7])), i977[7], i790[7], i706[7], i677[7])∧(U^Increasing(COND_LOAD3443ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i661[7], 1), 0), <(+(i661[7], 1), i663[7])), >=(i661[7], 0)), <(i661[7], i663[7])), >(+(i661[7], 1), 0)), <(+(i661[7], 1), i663[7])), >(i677[7], i706[7])), >(+(i661[7], 1), 0)), <(+(i661[7], 1), i663[7])), <(i661[7], i662[7])), i663[7], i304[7], i661[7], i662[7], java.lang.Object(ARRAY(i663[7], a3434data[7])), i977[7], i790[7], i706[7], i677[7])), ≥))

We simplified constraint (47) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(48)    (i662[7] + [-1] + [-1]i661[7] ≥ 0∧i663[7] + [-2] + [-1]i661[7] ≥ 0∧i661[7] ≥ 0∧i677[7] + [-1] + [-1]i706[7] ≥ 0∧i663[7] + [-1] + [-1]i661[7] ≥ 0∧i661[7] ≥ 0 ⇒ (U^Increasing(COND_LOAD3443ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i661[7], 1), 0), <(+(i661[7], 1), i663[7])), >=(i661[7], 0)), <(i661[7], i663[7])), >(+(i661[7], 1), 0)), <(+(i661[7], 1), i663[7])), >(i677[7], i706[7])), >(+(i661[7], 1), 0)), <(+(i661[7], 1), i663[7])), <(i661[7], i662[7])), i663[7], i304[7], i661[7], i662[7], java.lang.Object(ARRAY(i663[7], a3434data[7])), i977[7], i790[7], i706[7], i677[7])), ≥)∧[(-1)Bound*bni_42] + [bni_42]i663[7] + [(-1)bni_42]i304[7] ≥ 0∧[(-1)bso_43] ≥ 0)

We simplified constraint (48) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(49)    (i662[7] + [-1] + [-1]i661[7] ≥ 0∧i663[7] + [-2] + [-1]i661[7] ≥ 0∧i661[7] ≥ 0∧i677[7] + [-1] + [-1]i706[7] ≥ 0∧i663[7] + [-1] + [-1]i661[7] ≥ 0∧i661[7] ≥ 0 ⇒ (U^Increasing(COND_LOAD3443ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i661[7], 1), 0), <(+(i661[7], 1), i663[7])), >=(i661[7], 0)), <(i661[7], i663[7])), >(+(i661[7], 1), 0)), <(+(i661[7], 1), i663[7])), >(i677[7], i706[7])), >(+(i661[7], 1), 0)), <(+(i661[7], 1), i663[7])), <(i661[7], i662[7])), i663[7], i304[7], i661[7], i662[7], java.lang.Object(ARRAY(i663[7], a3434data[7])), i977[7], i790[7], i706[7], i677[7])), ≥)∧[(-1)Bound*bni_42] + [bni_42]i663[7] + [(-1)bni_42]i304[7] ≥ 0∧[(-1)bso_43] ≥ 0)

We simplified constraint (49) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(50)    (i662[7] + [-1] + [-1]i661[7] ≥ 0∧i663[7] + [-2] + [-1]i661[7] ≥ 0∧i661[7] ≥ 0∧i677[7] + [-1] + [-1]i706[7] ≥ 0∧i663[7] + [-1] + [-1]i661[7] ≥ 0∧i661[7] ≥ 0 ⇒ (U^Increasing(COND_LOAD3443ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i661[7], 1), 0), <(+(i661[7], 1), i663[7])), >=(i661[7], 0)), <(i661[7], i663[7])), >(+(i661[7], 1), 0)), <(+(i661[7], 1), i663[7])), >(i677[7], i706[7])), >(+(i661[7], 1), 0)), <(+(i661[7], 1), i663[7])), <(i661[7], i662[7])), i663[7], i304[7], i661[7], i662[7], java.lang.Object(ARRAY(i663[7], a3434data[7])), i977[7], i790[7], i706[7], i677[7])), ≥)∧[(-1)Bound*bni_42] + [bni_42]i663[7] + [(-1)bni_42]i304[7] ≥ 0∧[(-1)bso_43] ≥ 0)

We simplified constraint (50) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(51)    (i662[7] + [-1] + [-1]i661[7] ≥ 0∧i663[7] + [-2] + [-1]i661[7] ≥ 0∧i661[7] ≥ 0∧i677[7] + [-1] + [-1]i706[7] ≥ 0∧i663[7] + [-1] + [-1]i661[7] ≥ 0∧i661[7] ≥ 0 ⇒ (U^Increasing(COND_LOAD3443ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i661[7], 1), 0), <(+(i661[7], 1), i663[7])), >=(i661[7], 0)), <(i661[7], i663[7])), >(+(i661[7], 1), 0)), <(+(i661[7], 1), i663[7])), >(i677[7], i706[7])), >(+(i661[7], 1), 0)), <(+(i661[7], 1), i663[7])), <(i661[7], i662[7])), i663[7], i304[7], i661[7], i662[7], java.lang.Object(ARRAY(i663[7], a3434data[7])), i977[7], i790[7], i706[7], i677[7])), ≥)∧0 = 0∧[(-1)bni_42] = 0∧[(-1)Bound*bni_42] + [bni_42]i663[7] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_43] ≥ 0)

We simplified constraint (51) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(52)    (i662[7] ≥ 0∧i663[7] + [-2] + [-1]i661[7] ≥ 0∧i661[7] ≥ 0∧i677[7] + [-1] + [-1]i706[7] ≥ 0∧i663[7] + [-1] + [-1]i661[7] ≥ 0∧i661[7] ≥ 0 ⇒ (U^Increasing(COND_LOAD3443ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i661[7], 1), 0), <(+(i661[7], 1), i663[7])), >=(i661[7], 0)), <(i661[7], i663[7])), >(+(i661[7], 1), 0)), <(+(i661[7], 1), i663[7])), >(i677[7], i706[7])), >(+(i661[7], 1), 0)), <(+(i661[7], 1), i663[7])), <(i661[7], i662[7])), i663[7], i304[7], i661[7], i662[7], java.lang.Object(ARRAY(i663[7], a3434data[7])), i977[7], i790[7], i706[7], i677[7])), ≥)∧0 = 0∧[(-1)bni_42] = 0∧[(-1)Bound*bni_42] + [bni_42]i663[7] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_43] ≥ 0)

We simplified constraint (52) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(53)    (i662[7] ≥ 0∧i663[7] ≥ 0∧i661[7] ≥ 0∧i677[7] + [-1] + [-1]i706[7] ≥ 0∧[1] + i663[7] ≥ 0∧i661[7] ≥ 0 ⇒ (U^Increasing(COND_LOAD3443ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i661[7], 1), 0), <(+(i661[7], 1), i663[7])), >=(i661[7], 0)), <(i661[7], i663[7])), >(+(i661[7], 1), 0)), <(+(i661[7], 1), i663[7])), >(i677[7], i706[7])), >(+(i661[7], 1), 0)), <(+(i661[7], 1), i663[7])), <(i661[7], i662[7])), i663[7], i304[7], i661[7], i662[7], java.lang.Object(ARRAY(i663[7], a3434data[7])), i977[7], i790[7], i706[7], i677[7])), ≥)∧0 = 0∧[(-1)bni_42] = 0∧[(-1)Bound*bni_42 + (2)bni_42] + [bni_42]i661[7] + [bni_42]i663[7] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_43] ≥ 0)

We simplified constraint (53) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(54)    (i662[7] ≥ 0∧i663[7] ≥ 0∧i661[7] ≥ 0∧i677[7] ≥ 0∧[1] + i663[7] ≥ 0∧i661[7] ≥ 0 ⇒ (U^Increasing(COND_LOAD3443ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i661[7], 1), 0), <(+(i661[7], 1), i663[7])), >=(i661[7], 0)), <(i661[7], i663[7])), >(+(i661[7], 1), 0)), <(+(i661[7], 1), i663[7])), >(i677[7], i706[7])), >(+(i661[7], 1), 0)), <(+(i661[7], 1), i663[7])), <(i661[7], i662[7])), i663[7], i304[7], i661[7], i662[7], java.lang.Object(ARRAY(i663[7], a3434data[7])), i977[7], i790[7], i706[7], i677[7])), ≥)∧0 = 0∧[(-1)bni_42] = 0∧[(-1)Bound*bni_42 + (2)bni_42] + [bni_42]i661[7] + [bni_42]i663[7] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_43] ≥ 0)

We simplified constraint (54) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
(55)    (i662[7] ≥ 0∧i663[7] ≥ 0∧i661[7] ≥ 0∧i677[7] ≥ 0∧[1] + i663[7] ≥ 0∧i661[7] ≥ 0∧i706[7] ≥ 0 ⇒ (U^Increasing(COND_LOAD3443ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i661[7], 1), 0), <(+(i661[7], 1), i663[7])), >=(i661[7], 0)), <(i661[7], i663[7])), >(+(i661[7], 1), 0)), <(+(i661[7], 1), i663[7])), >(i677[7], i706[7])), >(+(i661[7], 1), 0)), <(+(i661[7], 1), i663[7])), <(i661[7], i662[7])), i663[7], i304[7], i661[7], i662[7], java.lang.Object(ARRAY(i663[7], a3434data[7])), i977[7], i790[7], i706[7], i677[7])), ≥)∧0 = 0∧[(-1)bni_42] = 0∧[(-1)Bound*bni_42 + (2)bni_42] + [bni_42]i661[7] + [bni_42]i663[7] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_43] ≥ 0)

(56)    (i662[7] ≥ 0∧i663[7] ≥ 0∧i661[7] ≥ 0∧i677[7] ≥ 0∧[1] + i663[7] ≥ 0∧i661[7] ≥ 0∧i706[7] ≥ 0 ⇒ (U^Increasing(COND_LOAD3443ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i661[7], 1), 0), <(+(i661[7], 1), i663[7])), >=(i661[7], 0)), <(i661[7], i663[7])), >(+(i661[7], 1), 0)), <(+(i661[7], 1), i663[7])), >(i677[7], i706[7])), >(+(i661[7], 1), 0)), <(+(i661[7], 1), i663[7])), <(i661[7], i662[7])), i663[7], i304[7], i661[7], i662[7], java.lang.Object(ARRAY(i663[7], a3434data[7])), i977[7], i790[7], i706[7], i677[7])), ≥)∧0 = 0∧[(-1)bni_42] = 0∧[(-1)Bound*bni_42 + (2)bni_42] + [bni_42]i661[7] + [bni_42]i663[7] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_43] ≥ 0)

For Pair COND_LOAD3443ARR2(TRUE, i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data)), i977, i790, i706, i677) → LOAD3657(i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434dataNew))) the following chains were created:

We consider the chain COND_LOAD3443ARR2(TRUE, i663[8], i304[8], i661[8], i662[8], java.lang.Object(ARRAY(i663[8], a3434data[8])), i977[8], i790[8], i706[8], i677[8]) → LOAD3657(i663[8], i304[8], i661[8], i662[8], java.lang.Object(ARRAY(i663[8], a3434dataNew[8]))) which results in the following constraint:
(57)    (COND_LOAD3443ARR2(TRUE, i663[8], i304[8], i661[8], i662[8], java.lang.Object(ARRAY(i663[8], a3434data[8])), i977[8], i790[8], i706[8], i677[8])≥NonInfC∧COND_LOAD3443ARR2(TRUE, i663[8], i304[8], i661[8], i662[8], java.lang.Object(ARRAY(i663[8], a3434data[8])), i977[8], i790[8], i706[8], i677[8])≥LOAD3657(i663[8], i304[8], i661[8], i662[8], java.lang.Object(ARRAY(i663[8], a3434dataNew[8])))∧(U^Increasing(LOAD3657(i663[8], i304[8], i661[8], i662[8], java.lang.Object(ARRAY(i663[8], a3434dataNew[8])))), ≥))

We simplified constraint (57) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(58)    ((U^Increasing(LOAD3657(i663[8], i304[8], i661[8], i662[8], java.lang.Object(ARRAY(i663[8], a3434dataNew[8])))), ≥)∧[(-1)bso_45] ≥ 0)

We simplified constraint (58) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(59)    ((U^Increasing(LOAD3657(i663[8], i304[8], i661[8], i662[8], java.lang.Object(ARRAY(i663[8], a3434dataNew[8])))), ≥)∧[(-1)bso_45] ≥ 0)

We simplified constraint (59) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(60)    ((U^Increasing(LOAD3657(i663[8], i304[8], i661[8], i662[8], java.lang.Object(ARRAY(i663[8], a3434dataNew[8])))), ≥)∧[(-1)bso_45] ≥ 0)

We simplified constraint (60) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(61)    ((U^Increasing(LOAD3657(i663[8], i304[8], i661[8], i662[8], java.lang.Object(ARRAY(i663[8], a3434dataNew[8])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_45] ≥ 0)

For Pair LOAD3443(i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data))) → COND_LOAD3443(&&(&&(>=(i661, i662), >(i304, 0)), >(+(i304, 1), 0)), i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data))) the following chains were created:

We consider the chain LOAD3443(i663[9], i304[9], i661[9], i662[9], java.lang.Object(ARRAY(i663[9], a3434data[9]))) → COND_LOAD3443(&&(&&(>=(i661[9], i662[9]), >(i304[9], 0)), >(+(i304[9], 1), 0)), i663[9], i304[9], i661[9], i662[9], java.lang.Object(ARRAY(i663[9], a3434data[9]))), COND_LOAD3443(TRUE, i663[10], i304[10], i661[10], i662[10], java.lang.Object(ARRAY(i663[10], a3434data[10]))) → LOAD2339(java.lang.Object(ARRAY(i663[10], a3434data[10])), i663[10], +(i304[10], 1)) which results in the following constraint:
(62)    (i304[9]=i304[10]∧i663[9]=i663[10]∧a3434data[9]=a3434data[10]∧&&(&&(>=(i661[9], i662[9]), >(i304[9], 0)), >(+(i304[9], 1), 0))=TRUE∧i661[9]=i661[10]∧i662[9]=i662[10] ⇒ LOAD3443(i663[9], i304[9], i661[9], i662[9], java.lang.Object(ARRAY(i663[9], a3434data[9])))≥NonInfC∧LOAD3443(i663[9], i304[9], i661[9], i662[9], java.lang.Object(ARRAY(i663[9], a3434data[9])))≥COND_LOAD3443(&&(&&(>=(i661[9], i662[9]), >(i304[9], 0)), >(+(i304[9], 1), 0)), i663[9], i304[9], i661[9], i662[9], java.lang.Object(ARRAY(i663[9], a3434data[9])))∧(U^Increasing(COND_LOAD3443(&&(&&(>=(i661[9], i662[9]), >(i304[9], 0)), >(+(i304[9], 1), 0)), i663[9], i304[9], i661[9], i662[9], java.lang.Object(ARRAY(i663[9], a3434data[9])))), ≥))

We simplified constraint (62) using rules (IV), (IDP_BOOLEAN) which results in the following new constraint:
(63)    (>(+(i304[9], 1), 0)=TRUE∧>=(i661[9], i662[9])=TRUE∧>(i304[9], 0)=TRUE ⇒ LOAD3443(i663[9], i304[9], i661[9], i662[9], java.lang.Object(ARRAY(i663[9], a3434data[9])))≥NonInfC∧LOAD3443(i663[9], i304[9], i661[9], i662[9], java.lang.Object(ARRAY(i663[9], a3434data[9])))≥COND_LOAD3443(&&(&&(>=(i661[9], i662[9]), >(i304[9], 0)), >(+(i304[9], 1), 0)), i663[9], i304[9], i661[9], i662[9], java.lang.Object(ARRAY(i663[9], a3434data[9])))∧(U^Increasing(COND_LOAD3443(&&(&&(>=(i661[9], i662[9]), >(i304[9], 0)), >(+(i304[9], 1), 0)), i663[9], i304[9], i661[9], i662[9], java.lang.Object(ARRAY(i663[9], a3434data[9])))), ≥))

We simplified constraint (63) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(64)    (i304[9] ≥ 0∧i661[9] + [-1]i662[9] ≥ 0∧i304[9] + [-1] ≥ 0 ⇒ (U^Increasing(COND_LOAD3443(&&(&&(>=(i661[9], i662[9]), >(i304[9], 0)), >(+(i304[9], 1), 0)), i663[9], i304[9], i661[9], i662[9], java.lang.Object(ARRAY(i663[9], a3434data[9])))), ≥)∧[(-1)Bound*bni_46] + [bni_46]i663[9] + [(-1)bni_46]i304[9] ≥ 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (64) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(65)    (i304[9] ≥ 0∧i661[9] + [-1]i662[9] ≥ 0∧i304[9] + [-1] ≥ 0 ⇒ (U^Increasing(COND_LOAD3443(&&(&&(>=(i661[9], i662[9]), >(i304[9], 0)), >(+(i304[9], 1), 0)), i663[9], i304[9], i661[9], i662[9], java.lang.Object(ARRAY(i663[9], a3434data[9])))), ≥)∧[(-1)Bound*bni_46] + [bni_46]i663[9] + [(-1)bni_46]i304[9] ≥ 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (65) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(66)    (i304[9] ≥ 0∧i661[9] + [-1]i662[9] ≥ 0∧i304[9] + [-1] ≥ 0 ⇒ (U^Increasing(COND_LOAD3443(&&(&&(>=(i661[9], i662[9]), >(i304[9], 0)), >(+(i304[9], 1), 0)), i663[9], i304[9], i661[9], i662[9], java.lang.Object(ARRAY(i663[9], a3434data[9])))), ≥)∧[(-1)Bound*bni_46] + [bni_46]i663[9] + [(-1)bni_46]i304[9] ≥ 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (66) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(67)    (i304[9] ≥ 0∧i661[9] + [-1]i662[9] ≥ 0∧i304[9] + [-1] ≥ 0 ⇒ (U^Increasing(COND_LOAD3443(&&(&&(>=(i661[9], i662[9]), >(i304[9], 0)), >(+(i304[9], 1), 0)), i663[9], i304[9], i661[9], i662[9], java.lang.Object(ARRAY(i663[9], a3434data[9])))), ≥)∧0 = 0∧[bni_46] = 0∧[(-1)Bound*bni_46] + [(-1)bni_46]i304[9] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (67) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(68)    ([1] + i304[9] ≥ 0∧i661[9] + [-1]i662[9] ≥ 0∧i304[9] ≥ 0 ⇒ (U^Increasing(COND_LOAD3443(&&(&&(>=(i661[9], i662[9]), >(i304[9], 0)), >(+(i304[9], 1), 0)), i663[9], i304[9], i661[9], i662[9], java.lang.Object(ARRAY(i663[9], a3434data[9])))), ≥)∧0 = 0∧[bni_46] = 0∧[(-1)Bound*bni_46 + (-1)bni_46] + [(-1)bni_46]i304[9] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (68) using rule (IDP_SMT_SPLIT) which results in the following new constraint:
(69)    ([1] + i304[9] ≥ 0∧i661[9] ≥ 0∧i304[9] ≥ 0 ⇒ (U^Increasing(COND_LOAD3443(&&(&&(>=(i661[9], i662[9]), >(i304[9], 0)), >(+(i304[9], 1), 0)), i663[9], i304[9], i661[9], i662[9], java.lang.Object(ARRAY(i663[9], a3434data[9])))), ≥)∧0 = 0∧[bni_46] = 0∧[(-1)Bound*bni_46 + (-1)bni_46] + [(-1)bni_46]i304[9] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_47] ≥ 0)

We simplified constraint (69) using rule (IDP_SMT_SPLIT) which results in the following new constraints:
(70)    ([1] + i304[9] ≥ 0∧i661[9] ≥ 0∧i304[9] ≥ 0∧i662[9] ≥ 0 ⇒ (U^Increasing(COND_LOAD3443(&&(&&(>=(i661[9], i662[9]), >(i304[9], 0)), >(+(i304[9], 1), 0)), i663[9], i304[9], i661[9], i662[9], java.lang.Object(ARRAY(i663[9], a3434data[9])))), ≥)∧0 = 0∧[bni_46] = 0∧[(-1)Bound*bni_46 + (-1)bni_46] + [(-1)bni_46]i304[9] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_47] ≥ 0)

(71)    ([1] + i304[9] ≥ 0∧i661[9] ≥ 0∧i304[9] ≥ 0∧i662[9] ≥ 0 ⇒ (U^Increasing(COND_LOAD3443(&&(&&(>=(i661[9], i662[9]), >(i304[9], 0)), >(+(i304[9], 1), 0)), i663[9], i304[9], i661[9], i662[9], java.lang.Object(ARRAY(i663[9], a3434data[9])))), ≥)∧0 = 0∧[bni_46] = 0∧[(-1)Bound*bni_46 + (-1)bni_46] + [(-1)bni_46]i304[9] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_47] ≥ 0)

For Pair COND_LOAD3443(TRUE, i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data))) → LOAD2339(java.lang.Object(ARRAY(i663, a3434data)), i663, +(i304, 1)) the following chains were created:

We consider the chain COND_LOAD3443(TRUE, i663[10], i304[10], i661[10], i662[10], java.lang.Object(ARRAY(i663[10], a3434data[10]))) → LOAD2339(java.lang.Object(ARRAY(i663[10], a3434data[10])), i663[10], +(i304[10], 1)) which results in the following constraint:
(72)    (COND_LOAD3443(TRUE, i663[10], i304[10], i661[10], i662[10], java.lang.Object(ARRAY(i663[10], a3434data[10])))≥NonInfC∧COND_LOAD3443(TRUE, i663[10], i304[10], i661[10], i662[10], java.lang.Object(ARRAY(i663[10], a3434data[10])))≥LOAD2339(java.lang.Object(ARRAY(i663[10], a3434data[10])), i663[10], +(i304[10], 1))∧(U^Increasing(LOAD2339(java.lang.Object(ARRAY(i663[10], a3434data[10])), i663[10], +(i304[10], 1))), ≥))

We simplified constraint (72) using rule (POLY_CONSTRAINTS) which results in the following new constraint:
(73)    ((U^Increasing(LOAD2339(java.lang.Object(ARRAY(i663[10], a3434data[10])), i663[10], +(i304[10], 1))), ≥)∧[1 + (-1)bso_49] ≥ 0)

We simplified constraint (73) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:
(74)    ((U^Increasing(LOAD2339(java.lang.Object(ARRAY(i663[10], a3434data[10])), i663[10], +(i304[10], 1))), ≥)∧[1 + (-1)bso_49] ≥ 0)

We simplified constraint (74) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:
(75)    ((U^Increasing(LOAD2339(java.lang.Object(ARRAY(i663[10], a3434data[10])), i663[10], +(i304[10], 1))), ≥)∧[1 + (-1)bso_49] ≥ 0)

We simplified constraint (75) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:
(76)    ((U^Increasing(LOAD2339(java.lang.Object(ARRAY(i663[10], a3434data[10])), i663[10], +(i304[10], 1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_49] ≥ 0)

To summarize, we get the following constraints P_≥ for the following pairs.

LOAD2339(java.lang.Object(ARRAY(i303, a2291data)), i303, i304) → COND_LOAD2339(&&(>(i304, 0), <(i304, i303)), java.lang.Object(ARRAY(i303, a2291data)), i303, i304)
- (i304[0] ≥ 0∧i303[0] ≥ 0 ⇒ (U^Increasing(COND_LOAD2339(&&(>(i304[0], 0), <(i304[0], i303[0])), java.lang.Object(ARRAY(i303[0], a2291data[0])), i303[0], i304[0])), ≥)∧0 = 0∧[(-1)Bound*bni_28 + bni_28] + [bni_28]i303[0] ≥ 0∧0 = 0∧[(-1)bso_29] ≥ 0)
COND_LOAD2339(TRUE, java.lang.Object(ARRAY(i303, a2291data)), i303, i304) → LOAD3443(i303, i304, 0, -(i303, i304), java.lang.Object(ARRAY(i303, a2291data)))
- ((U^Increasing(LOAD3443(i303[1], i304[1], 0, -(i303[1], i304[1]), java.lang.Object(ARRAY(i303[1], a2291data[1])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_31] ≥ 0)
LOAD3657(i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data))) → LOAD3443(i663, i304, +(i661, 1), i662, java.lang.Object(ARRAY(i663, a3434data)))
- ((U^Increasing(LOAD3443(i663[2], i304[2], +(i661[2], 1), i662[2], java.lang.Object(ARRAY(i663[2], a3434data[2])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_33] ≥ 0)
LOAD3443(i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data))) → LOAD3443ARR1(i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data)), i706, i677)
- ((U^Increasing(LOAD3443ARR1(i663[3], i304[3], i661[3], i662[3], java.lang.Object(ARRAY(i663[3], a3434data[3])), i706[3], i677[3])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_35] ≥ 0)
LOAD3443ARR1(i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data)), i706, i677) → COND_LOAD3443ARR1(&&(&&(&&(&&(&&(&&(<=(i677, i706), >(+(i661, 1), 0)), <(+(i661, 1), i663)), >=(i661, 0)), <(i661, i663)), <(i661, i662)), >(+(i661, 1), 0)), i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data)), i706, i677)
- (i661[4] ≥ 0∧i662[4] ≥ 0∧[1] + i663[4] ≥ 0∧i661[4] ≥ 0∧i663[4] ≥ 0∧i706[4] ≥ 0∧i677[4] ≥ 0 ⇒ (U^Increasing(COND_LOAD3443ARR1(&&(&&(&&(&&(&&(&&(<=(i677[4], i706[4]), >(+(i661[4], 1), 0)), <(+(i661[4], 1), i663[4])), >=(i661[4], 0)), <(i661[4], i663[4])), <(i661[4], i662[4])), >(+(i661[4], 1), 0)), i663[4], i304[4], i661[4], i662[4], java.lang.Object(ARRAY(i663[4], a3434data[4])), i706[4], i677[4])), ≥)∧0 = 0∧[(-1)bni_36] = 0∧[(-1)Bound*bni_36 + (2)bni_36] + [bni_36]i661[4] + [bni_36]i663[4] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_37] ≥ 0)
- (i661[4] ≥ 0∧i662[4] ≥ 0∧[1] + i663[4] ≥ 0∧i661[4] ≥ 0∧i663[4] ≥ 0∧i706[4] ≥ 0∧i677[4] ≥ 0 ⇒ (U^Increasing(COND_LOAD3443ARR1(&&(&&(&&(&&(&&(&&(<=(i677[4], i706[4]), >(+(i661[4], 1), 0)), <(+(i661[4], 1), i663[4])), >=(i661[4], 0)), <(i661[4], i663[4])), <(i661[4], i662[4])), >(+(i661[4], 1), 0)), i663[4], i304[4], i661[4], i662[4], java.lang.Object(ARRAY(i663[4], a3434data[4])), i706[4], i677[4])), ≥)∧0 = 0∧[(-1)bni_36] = 0∧[(-1)Bound*bni_36 + (2)bni_36] + [bni_36]i661[4] + [bni_36]i663[4] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_37] ≥ 0)
COND_LOAD3443ARR1(TRUE, i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data)), i706, i677) → LOAD3443(i663, i304, +(i661, 1), i662, java.lang.Object(ARRAY(i663, a3434data)))
- ((U^Increasing(LOAD3443(i663[5], i304[5], +(i661[5], 1), i662[5], java.lang.Object(ARRAY(i663[5], a3434data[5])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_39] ≥ 0)
LOAD3443(i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data))) → LOAD3443ARR2(i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data)), i977, i790, i706, i677)
- ((U^Increasing(LOAD3443ARR2(i663[6], i304[6], i661[6], i662[6], java.lang.Object(ARRAY(i663[6], a3434data[6])), i977[6], i790[6], i706[6], i677[6])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_41] ≥ 0)
LOAD3443ARR2(i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data)), i977, i790, i706, i677) → COND_LOAD3443ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i661, 1), 0), <(+(i661, 1), i663)), >=(i661, 0)), <(i661, i663)), >(+(i661, 1), 0)), <(+(i661, 1), i663)), >(i677, i706)), >(+(i661, 1), 0)), <(+(i661, 1), i663)), <(i661, i662)), i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data)), i977, i790, i706, i677)
- (i662[7] ≥ 0∧i663[7] ≥ 0∧i661[7] ≥ 0∧i677[7] ≥ 0∧[1] + i663[7] ≥ 0∧i661[7] ≥ 0∧i706[7] ≥ 0 ⇒ (U^Increasing(COND_LOAD3443ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i661[7], 1), 0), <(+(i661[7], 1), i663[7])), >=(i661[7], 0)), <(i661[7], i663[7])), >(+(i661[7], 1), 0)), <(+(i661[7], 1), i663[7])), >(i677[7], i706[7])), >(+(i661[7], 1), 0)), <(+(i661[7], 1), i663[7])), <(i661[7], i662[7])), i663[7], i304[7], i661[7], i662[7], java.lang.Object(ARRAY(i663[7], a3434data[7])), i977[7], i790[7], i706[7], i677[7])), ≥)∧0 = 0∧[(-1)bni_42] = 0∧[(-1)Bound*bni_42 + (2)bni_42] + [bni_42]i661[7] + [bni_42]i663[7] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_43] ≥ 0)
- (i662[7] ≥ 0∧i663[7] ≥ 0∧i661[7] ≥ 0∧i677[7] ≥ 0∧[1] + i663[7] ≥ 0∧i661[7] ≥ 0∧i706[7] ≥ 0 ⇒ (U^Increasing(COND_LOAD3443ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i661[7], 1), 0), <(+(i661[7], 1), i663[7])), >=(i661[7], 0)), <(i661[7], i663[7])), >(+(i661[7], 1), 0)), <(+(i661[7], 1), i663[7])), >(i677[7], i706[7])), >(+(i661[7], 1), 0)), <(+(i661[7], 1), i663[7])), <(i661[7], i662[7])), i663[7], i304[7], i661[7], i662[7], java.lang.Object(ARRAY(i663[7], a3434data[7])), i977[7], i790[7], i706[7], i677[7])), ≥)∧0 = 0∧[(-1)bni_42] = 0∧[(-1)Bound*bni_42 + (2)bni_42] + [bni_42]i661[7] + [bni_42]i663[7] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_43] ≥ 0)
COND_LOAD3443ARR2(TRUE, i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data)), i977, i790, i706, i677) → LOAD3657(i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434dataNew)))
- ((U^Increasing(LOAD3657(i663[8], i304[8], i661[8], i662[8], java.lang.Object(ARRAY(i663[8], a3434dataNew[8])))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_45] ≥ 0)
LOAD3443(i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data))) → COND_LOAD3443(&&(&&(>=(i661, i662), >(i304, 0)), >(+(i304, 1), 0)), i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data)))
- ([1] + i304[9] ≥ 0∧i661[9] ≥ 0∧i304[9] ≥ 0∧i662[9] ≥ 0 ⇒ (U^Increasing(COND_LOAD3443(&&(&&(>=(i661[9], i662[9]), >(i304[9], 0)), >(+(i304[9], 1), 0)), i663[9], i304[9], i661[9], i662[9], java.lang.Object(ARRAY(i663[9], a3434data[9])))), ≥)∧0 = 0∧[bni_46] = 0∧[(-1)Bound*bni_46 + (-1)bni_46] + [(-1)bni_46]i304[9] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_47] ≥ 0)
- ([1] + i304[9] ≥ 0∧i661[9] ≥ 0∧i304[9] ≥ 0∧i662[9] ≥ 0 ⇒ (U^Increasing(COND_LOAD3443(&&(&&(>=(i661[9], i662[9]), >(i304[9], 0)), >(+(i304[9], 1), 0)), i663[9], i304[9], i661[9], i662[9], java.lang.Object(ARRAY(i663[9], a3434data[9])))), ≥)∧0 = 0∧[bni_46] = 0∧[(-1)Bound*bni_46 + (-1)bni_46] + [(-1)bni_46]i304[9] ≥ 0∧0 = 0∧0 = 0∧[(-1)bso_47] ≥ 0)
COND_LOAD3443(TRUE, i663, i304, i661, i662, java.lang.Object(ARRAY(i663, a3434data))) → LOAD2339(java.lang.Object(ARRAY(i663, a3434data)), i663, +(i304, 1))
- ((U^Increasing(LOAD2339(java.lang.Object(ARRAY(i663[10], a3434data[10])), i663[10], +(i304[10], 1))), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_49] ≥ 0)

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0
POL(FALSE) = 0
POL(LOAD2339(x₁, x₂, x₃)) = [-1] + [-1]x₁ + [-1]x₃
POL(java.lang.Object(x₁)) = x₁
POL(ARRAY(x₁, x₂)) = [-1] + [-1]x₁
POL(COND_LOAD2339(x₁, x₂, x₃, x₄)) = [-1] + [-1]x₂ + [-1]x₄
POL(&&(x₁, x₂)) = 0
POL(>(x₁, x₂)) = [-1]
POL(0) = 0
POL(<(x₁, x₂)) = [-1]
POL(LOAD3443(x₁, x₂, x₃, x₄, x₅)) = [-1] + [-1]x₅ + [-1]x₂
POL(-(x₁, x₂)) = x₁ + [-1]x₂
POL(LOAD3657(x₁, x₂, x₃, x₄, x₅)) = [-1] + [-1]x₅ + [-1]x₂
POL(+(x₁, x₂)) = x₁ + x₂
POL(1) = [1]
POL(LOAD3443ARR1(x₁, x₂, x₃, x₄, x₅, x₆, x₇)) = [-1] + [-1]x₅ + [-1]x₂
POL(COND_LOAD3443ARR1(x₁, x₂, x₃, x₄, x₅, x₆, x₇, x₈)) = [-1] + [-1]x₆ + [-1]x₃
POL(<=(x₁, x₂)) = [-1]
POL(>=(x₁, x₂)) = [-1]
POL(LOAD3443ARR2(x₁, x₂, x₃, x₄, x₅, x₆, x₇, x₈, x₉)) = [-1] + [-1]x₅ + [-1]x₂
POL(COND_LOAD3443ARR2(x₁, x₂, x₃, x₄, x₅, x₆, x₇, x₈, x₉, x₁₀)) = [-1] + [-1]x₆ + [-1]x₃
POL(COND_LOAD3443(x₁, x₂, x₃, x₄, x₅, x₆)) = [-1] + [-1]x₆ + [-1]x₃

The following pairs are in P_>:

COND_LOAD3443(TRUE, i663[10], i304[10], i661[10], i662[10], java.lang.Object(ARRAY(i663[10], a3434data[10]))) → LOAD2339(java.lang.Object(ARRAY(i663[10], a3434data[10])), i663[10], +(i304[10], 1))

The following pairs are in P_bound:

LOAD2339(java.lang.Object(ARRAY(i303[0], a2291data[0])), i303[0], i304[0]) → COND_LOAD2339(&&(>(i304[0], 0), <(i304[0], i303[0])), java.lang.Object(ARRAY(i303[0], a2291data[0])), i303[0], i304[0])

The following pairs are in P_≥:

LOAD2339(java.lang.Object(ARRAY(i303[0], a2291data[0])), i303[0], i304[0]) → COND_LOAD2339(&&(>(i304[0], 0), <(i304[0], i303[0])), java.lang.Object(ARRAY(i303[0], a2291data[0])), i303[0], i304[0])
COND_LOAD2339(TRUE, java.lang.Object(ARRAY(i303[1], a2291data[1])), i303[1], i304[1]) → LOAD3443(i303[1], i304[1], 0, -(i303[1], i304[1]), java.lang.Object(ARRAY(i303[1], a2291data[1])))
LOAD3657(i663[2], i304[2], i661[2], i662[2], java.lang.Object(ARRAY(i663[2], a3434data[2]))) → LOAD3443(i663[2], i304[2], +(i661[2], 1), i662[2], java.lang.Object(ARRAY(i663[2], a3434data[2])))
LOAD3443(i663[3], i304[3], i661[3], i662[3], java.lang.Object(ARRAY(i663[3], a3434data[3]))) → LOAD3443ARR1(i663[3], i304[3], i661[3], i662[3], java.lang.Object(ARRAY(i663[3], a3434data[3])), i706[3], i677[3])
LOAD3443ARR1(i663[4], i304[4], i661[4], i662[4], java.lang.Object(ARRAY(i663[4], a3434data[4])), i706[4], i677[4]) → COND_LOAD3443ARR1(&&(&&(&&(&&(&&(&&(<=(i677[4], i706[4]), >(+(i661[4], 1), 0)), <(+(i661[4], 1), i663[4])), >=(i661[4], 0)), <(i661[4], i663[4])), <(i661[4], i662[4])), >(+(i661[4], 1), 0)), i663[4], i304[4], i661[4], i662[4], java.lang.Object(ARRAY(i663[4], a3434data[4])), i706[4], i677[4])
COND_LOAD3443ARR1(TRUE, i663[5], i304[5], i661[5], i662[5], java.lang.Object(ARRAY(i663[5], a3434data[5])), i706[5], i677[5]) → LOAD3443(i663[5], i304[5], +(i661[5], 1), i662[5], java.lang.Object(ARRAY(i663[5], a3434data[5])))
LOAD3443(i663[6], i304[6], i661[6], i662[6], java.lang.Object(ARRAY(i663[6], a3434data[6]))) → LOAD3443ARR2(i663[6], i304[6], i661[6], i662[6], java.lang.Object(ARRAY(i663[6], a3434data[6])), i977[6], i790[6], i706[6], i677[6])
LOAD3443ARR2(i663[7], i304[7], i661[7], i662[7], java.lang.Object(ARRAY(i663[7], a3434data[7])), i977[7], i790[7], i706[7], i677[7]) → COND_LOAD3443ARR2(&&(&&(&&(&&(&&(&&(&&(&&(&&(>(+(i661[7], 1), 0), <(+(i661[7], 1), i663[7])), >=(i661[7], 0)), <(i661[7], i663[7])), >(+(i661[7], 1), 0)), <(+(i661[7], 1), i663[7])), >(i677[7], i706[7])), >(+(i661[7], 1), 0)), <(+(i661[7], 1), i663[7])), <(i661[7], i662[7])), i663[7], i304[7], i661[7], i662[7], java.lang.Object(ARRAY(i663[7], a3434data[7])), i977[7], i790[7], i706[7], i677[7])
COND_LOAD3443ARR2(TRUE, i663[8], i304[8], i661[8], i662[8], java.lang.Object(ARRAY(i663[8], a3434data[8])), i977[8], i790[8], i706[8], i677[8]) → LOAD3657(i663[8], i304[8], i661[8], i662[8], java.lang.Object(ARRAY(i663[8], a3434dataNew[8])))
LOAD3443(i663[9], i304[9], i661[9], i662[9], java.lang.Object(ARRAY(i663[9], a3434data[9]))) → COND_LOAD3443(&&(&&(>=(i661[9], i662[9]), >(i304[9], 0)), >(+(i304[9], 1), 0)), i663[9], i304[9], i661[9], i662[9], java.lang.Object(ARRAY(i663[9], a3434data[9])))

There are no usable rules.

(17) Complex Obligation (AND)

(18) Obligation:

IDP problem:
The following function symbols are pre-defined:

!=	~	Neq: (Integer, Integer) -> Boolean
*	~	Mul: (Integer, Integer) -> Integer
>=	~	Ge: (Integer, Integer) -> Boolean
-1	~	UnaryMinus: (Integer) -> Integer
\|	~	Bwor: (Integer, Integer) -> Integer
/	~	Div: (Integer, Integer) -> Integer
=	~	Eq: (Integer, Integer) -> Boolean
	~	Bwxor: (Integer, Integer) -> Integer
\|\|	~	Lor: (Boolean, Boolean) -> Boolean
!	~	Lnot: (Boolean) -> Boolean
<	~	Lt: (Integer, Integer) -> Boolean
-	~	Sub: (Integer, Integer) -> Integer
<=	~	Le: (Integer, Integer) -> Boolean
>	~	Gt: (Integer, Integer) -> Boolean
~	~	Bwnot: (Integer) -> Integer
%	~	Mod: (Integer, Integer) -> Integer
&	~	Bwand: (Integer, Integer) -> Integer
+	~	Add: (Integer, Integer) -> Integer
&&	~	Land: (Boolean, Boolean) -> Boolean